| let ( let+ ) = Option.bind | |
| module Expr = struct | |
| type app = A | |
| type fun' = F | |
| type name = N | |
| type 'variant reducible = A : app reducible | |
| type 'variant irreducible = | |
| | F : fun' irreducible |
| module type TYPE = sig | |
| type t | |
| end | |
| type 't module' = (module TYPE with type t = 't) | |
| type 'a first = 'b constraint 'a = 'b * _ | |
| type 'a second = 'c constraint 'a = _ * 'c | |
| module Runtype = struct | |
| type 'a t = |
| let get_char () = | |
| let attr = Unix.tcgetattr Unix.stdin in | |
| let () = | |
| Unix.tcsetattr | |
| Unix.stdin | |
| Unix.TCSADRAIN | |
| { attr with Unix.c_icanon = false } | |
| in | |
| let res = input_byte stdin in | |
| Unix.tcsetattr Unix.stdin Unix.TCSADRAIN attr; |
| module Option = struct | |
| include Option | |
| let or_else : type item. (unit -> item t) -> item t -> item t = | |
| fun rightf left -> | |
| match left with | |
| | None -> rightf () | |
| | _ -> left | |
| ;; |
| tokens: | |
| INFINITY ≔ '∞' | |
| ZERO ≔ '0' | |
| ONE ≔ '1' | |
| NONZERO ≔ /[1-9][0-9]*/ | |
| QUESTION_MARK ≔ '?' | |
| BANG ≔ '!' | |
| NAME ≔ /[A-Za-z_][A-Za-z0-9_']*/ | |
| CONTAINS ≔ '∋' |
| Require Import Utf8. | |
| (** [Eqw f x y] represents the equivalence x y up to an isomorphism f. *) | |
| Inductive Eqw {A B : Type} (f : A → B) : A → A → Prop := | |
| | Refl (x y : A) : f x = f y → Eqw f x y. | |
| (** Notation for convenience. Same level as equality. *) | |
| Notation "x = y 'up' 'to' f" := (Eqw f x y). | |
| (** Utilitary functions for the theorems below. *) |
| Require Import String. | |
| Inductive Term : nat -> Type := | |
| | App : forall {n m : nat}, Term (S n) -> Term m -> Term (n + m) | |
| | Fun : forall {n : nat}, Term 0 -> Term n -> Term (S n) | |
| | Var : string -> Term 0. |
A cartesian type is a generalized type product where one inhabitant, called origin is common to all the types involved (called axes). A cocartesian type is a generalized type sum with a common origin to all axes.
That is, A * ... * Z is a cartesian type if there exists one inhabitant i common to every axis — i_A = i_B = ... = i_Z.
# x is introduced to the environment
{ ..?e } → { x := 3 ; ..?e }
# y too ; ?e is not the same row variable as the one above
{ ..?e } → { y := 5 ; ..?e }
# matching the current context on one that contains an x and a y
# which allows us to add them to introduce y
{ x ; y ; ..?e } → { z := x + y ; ..?e }
| let ( or ) option default = Option.value option ~default | |
| module Int = struct | |
| include Int | |
| let compare i1 i2 = | |
| let as_int = compare i1 i2 in | |
| if as_int > 0 then `Greater else if as_int < 0 then `Less else `Equal | |
| ;; |