ronenlh

/build

ronenlh

/build

ronenlh

Verifying my Blockstack ID is secured with the address 1H7aav5MLqnEpPd5JGaLwFv4VdyaFxttFz https://explorer.blockstack.org/address/1H7aav5MLqnEpPd5JGaLwFv4VdyaFxttFz

ronenlh

int uv_run(uv_loop_t* loop, uv_run_mode mode) {
  int timeout;
  int r;
  int ran_pending;

  r = uv__loop_alive(loop);
  if (!r)
    uv__update_time(loop);

  while (r != 0 && loop->stop_flag == 0) {

ronenlh

{ lib
, stdenv
, fetchurl
, testVersion
, hello
}:

stdenv.mkDerivation rec {
  pname = "hello";
  version = "2.10";

ronenlh

{ }:
let
    pkgs = import (builtins.fetchGit {
        name = "nixpkgs-with-cmake-3.18.2";
        url = "https://github.com/NixOS/nixpkgs/";
        ref = "refs/heads/nixpkgs-unstable";
        rev = "2c162d49cd5b979eb66ff1653aecaeaa01690fcc";
    }) {};

    pkgs_ninja = import (builtins.fetchGit {

ronenlh

// TypeScript

// Types
type Coin = { readonly tag: "Coin" };
type HotWater = { readonly tag: "HotWater" };
type Noodles = { readonly tag: "Noodles" };
type InstantNoodles = (hw: HotWater) => Noodles;

// Theorem: Given an instant noodle vending machine I can make a coin-&-hot-water-to-noodles system
function theorem(vendingMachine: (coin: Coin) => InstantNoodles): (assets: { coin: Coin; hotWater: HotWater }) => Noodles {

ronenlh

// TypeScript

// Types
type P = { readonly tag: "P" };
type Q = { readonly tag: "Q" };
type R = { readonly tag: "R" };

type Theorem = (h: (p: P) => (q: Q) => R) => ((hpq: { left: P; right: Q }) => R);

// Theorem

ronenlh

// TypeScript Type
(h: (p: P) => (q: Q) => R) => ((hpq: { left: P; right: Q }) => R)

// Logic theorem
(P → Q → R) → (P ∧ Q → R)

ronenlh

-- Lean
example : (P → Q → R) → (P ∧ Q → R) :=
  fun myFunc myParam =>
    myFunc myParam.left myParam.right