Merge branch 'master' of https://github.com/Kindelia/Kind2

Cargo.lock

@@ -176,7 +176,7 @@ dependencies = [
 
 [[package]]
 name = "kind2"
-version = "0.2.69"
+version = "0.2.70"
 dependencies = [
  "clap",
  "highlight_error",

Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "kind2"
-version = "0.2.69"
+version = "0.2.71"
 edition = "2021"
 description = "A pure functional functional language that uses the HVM."
 repository = "https://github.com/Kindelia/Kind2"
@@ -10,7 +10,7 @@ keywords = ["functional", "language", "type-theory", "proof-assistant"]
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
 [dependencies]
-hvm = "0.1.80"
+hvm = "0.1.81"
 #hvm = { path = "../hvm" }
 highlight_error = "0.1.1"
 clap = { version = "3.1.8", features = ["derive"] }

README.md

@@ -1,62 +1,64 @@
 Kind2
 =====
 
-Kind2 is a pure functional, lazy, non-garbage-collected, general-purpose,
-dependently typed programming language focusing on performance and usability. It
-features a blazingly fast type-checker based on **optimal
-[normalization-by-evaluation](https://en.wikipedia.org/wiki/Normalisation_by_evaluation)**. It can also
-compile programs to [HVM](https://github.com/kindelia/hvm) and [Kindelia](https://github.com/kindelia/kindelia),
-and can be used to prove and verify mathematical theorems.
+**Kind2** is a **functional programming language** and **proof assistant**.
+
+It is a complete rewrite of [Kind1](https://github.com/kindelia/kind-legacy), based on
+[HVM](https://github.com/kindelia/hvm), a **lazy**, **non-garbage-collected** and **massively parallel** virtual
+machine. In [our benchmarks](https://github.com/kindelia/functional-benchmarks), its type-checker outperforms every
+alternative proof assistant by a far margin, and its programs can offer exponential speedups over Haskell's GHC. Kind2
+unleashes the [inherent parallelism of the Lambda
+Calculus](https://github.com/VictorTaelin/Symmetric-Interaction-Calculus) to become the ultimate programming language of
+the next century.
+
+**Welcome to the inevitable parallel, functional future of computers!**
 
 Examples
 --------
 
-Pure functions can be defined using an equational notation that resembles [Haskell](https://www.haskell.org/):
+Pure functions are defined via equations, as in [Haskell](https://www.haskell.org/):
 
-```idris
-List.map <a: Type> <b: Type> (x: (List a)) (f: (x: a) b) : (List b)
-List.map a b (Nil t)       f = (Nil b)
-List.map a b (Cons t x xs) f = (Cons b (f x) (List.map xs f))
+```javascript
+// Applies a function to every element of a list
+map <a> <b> (list: List a) (f: a -> b) : List b
+map a b Nil              f = Nil
+map a b (Cons head tail) f = Cons (f x) (map tail f)
 ```
 
-Mathematical theorems can be proved via inductive reasoning, as in [Idris](https://www.idris-lang.org/) and [Agda](https://wiki.portal.chalmers.se/agda/pmwiki.php):
+Side-effective programs are written via monadic monads, resembling [Rust](https://www.rust-lang.org/) and [TypeScript](https://www.typescriptlang.org/):
 
-```idris
-Nat.commutes (a: Nat) (b: Nat) : (Nat.add a b) == (Nat.add b a)
-Nat.commutes Zero     b = (Nat.comm.a b)
-Nat.commutes (Succ a) b =
-  let e0 = (Equal.apply @x(Succ x) (Nat.commutes a b))
-  let e1 = (Equal.mirror (Nat.commutes.b b a))
-  (Equal.chain e0 e1)
-```
-
-Normal programs can be written in a monadic syntax that is inspired by [Rust](https://www.rust-lang.org/) and [TypeScript](https://www.typescriptlang.org/):
-
-```idris
-Main : (IO (Result () String)) {
-  ask limit = (IO.prompt "Enter limit:")
+```javascript
+// Prints the double of every numbet up to a limit
+Main : IO (Result () String) {
+  ask limit = IO.prompt "Enter limit:"
   for x in (List.range limit) {
-    (IO.print "{} * 2 = {}" x (Nat.double x))
+    IO.print "{} * 2 = {}" x (Nat.double x)
   }
-  return (Ok ())
+  return Ok ()
 }
 ```
 
+Theorems can be proved inductivelly, as in [Agda](https://wiki.portal.chalmers.se/agda/pmwiki.php) and [Idris](https://www.idris-lang.org/):
+
+```javascript
+// Black Friday Theorem. Proof that, for every Nat n: n * 2 / 2 == n.
+black_friday_theorem (n: Nat) : Equal Nat (Nat.half (Nat.double n)) n
+black_friday_theorem Nat.zero     = Equal.refl
+black_friday_theorem (Nat.succ n) = Equal.apply (x => Nat.succ x) (black_friday_theorem n)
+```
+
 For more examples, check the [Wikind](https://github.com/kindelia/wikind).
 
-Installation
-------------
+Usage
+-----
 
-Install [Rust](https://www.rust-lang.org/tools/install) first, then enter:
+First, install [Rust](https://www.rust-lang.org/tools/install) first, then enter:
 
 ```
 cargo install kind2
 ```
 
-Enter `kind2` on the terminal to make sure it worked.
-
-Usage
------
+Then, use any of the commands below:
 
 Command    | Usage                     | Note
 ---------- | ------------------------- | --------------------------------------------------------------
@@ -64,9 +66,13 @@ Check      | `kind2 check  file.kind2` | Checks all definitions.
 Eval       | `kind2 eval   file.kind2` | Runs using the type-checker's evaluator.
 Run        | `kind2 run    file.kind2` | Runs using HVM's evaluator, on Rust-mode.
 To-HVM     | `kind2 to-hvm file.kind2` | Generates a [.hvm](https://github.com/kindelia/hvm) file. Can then be compiled to C.
-To-KDL     | `kind2 to-kdl file.kind2` | Generates a [.kdl](https://github.com/kindelia/kindelia) file. Can then be deployed to Kindelia.
+To-KDL     | `kind2 to-kdl file.kind2` | Generates a [.kdl](https://github.com/kindelia/kindelia) file. Can then be deployed to [Kindelia](https://github.com/kindelia/kindelia).
 
-Benchmarks
-----------
+Executables can be generated via HVM:
 
-In preliminary [benchmarks](/bench), Kind2's type-checker has outperformed Agda, Idris by 90x to 900x, which is an expressive difference. That said, we only tested a few small programs, so there isn't enough data to draw a conclusion yet. We're working on a more extensive benchmark suite. 
+```
+kind2 to-hvm file.kind2
+hvm compile file.hvm
+clang -O2 file.c -o file
+./file
+```

bench/README.md

@@ -1,61 +0,0 @@
-Bench
-=====
-
-Benchmarks of Kind2 vs other proof assistants. These benchmarks measure the time
-each assistant takes to verify a given file. Replicate as follows:
-
-### Agda
-
-```
-time agda -i src file.agda
-```
-
-### Coq
-
-```
-time coqtop -l file.v -batch -type-in-type
-```
-
-### Idris2
-
-```
-time idris2 --check file.idr
-```
-
-### Lean
-
-```
-time lean file.lean
-```
-
-### Kind2
-
-```
-time kind2 check file.kind2
-```
-
-### Kind2-C
-
-```
-kind2 gen-checker file.kind2
-hvm compile file.check.hvm
-clang file.check.c -O3 -o check
-time ./check
-```
-
-Results
-=======
-
-### nat_exp
-
-Computes `3 ^ 8`, using the Nat type, on the type level.
-
-```
-language | time
--------- | --------
-Kind2-C  |   0.17 s
-Kind2    |   0.58 s
-Agda     |  15.55 s
-Idris2   |  67.40 s
-Lean     |  timeout
-```

bench/conv_eval.idr

@@ -1,239 +0,0 @@
-CBool : Type
-CBool = (B : Type) -> B -> B -> B
-
-toBool : CBool -> Bool
-toBool = \b => b Bool True False
-
-ctrue : CBool
-ctrue = \b, t, f => t
-
-and : CBool -> CBool -> CBool
-and = \a, b, bb, t, f => a bb (b bb t f) f
-
-CNat : Type
-CNat = (n : Type) -> (n -> n) -> n -> n
-
-add : CNat -> CNat -> CNat
-add = \a, b, n, s, z => a n s (b n s z)
-
-cmul : CNat -> CNat -> CNat
-cmul = \a, b, n, s => a n (b n s)
-
-suc : CNat -> CNat
-suc = \a, n, s, z => s (a n s z)
-
-CEq : {A : Type} -> A -> A -> Type
-CEq = \x, y => (P : A -> Type) -> P x -> P y
-
-crefl : {A : Type} -> {x : A} -> CEq {A} x x
-crefl = \p, px => px
-
-n2 : CNat
-n2 = \n, s, z => s (s z)
-
-n3 : CNat
-n3 = \n, s, z => s (s (s z))
-
-n4 : CNat
-n4 = \n, s, z => s (s (s (s z)))
-
-n5 : CNat
-n5 = \n, s, z => s (s (s (s (s z))))
-
-n10 : CNat
-n10  = cmul n2 n5
-
-n10b : CNat
-n10b = cmul n5 n2
-
-n15 : CNat
-n15 = add n10  n5
-
-n15b : CNat
-n15b   = add n10b n5
-
-n18 : CNat
-n18    = add n15  n3
-
-n18b : CNat
-n18b   = add n15b n3
-
-n19 : CNat
-n19    = add n15  n4
-
-n19b : CNat
-n19b   = add n15b n4
-
-n20 : CNat
-n20    = cmul n2 n10
-
-n20b : CNat
-n20b   = cmul n2 n10b
-
-n21 : CNat
-n21    = suc n20
-
-n21b : CNat
-n21b   = suc n20b
-
-n22 : CNat
-n22    = suc n21
-
-n22b : CNat
-n22b   = suc n21b
-
-n23 : CNat
-n23    = suc n22
-
-n23b : CNat
-n23b   = suc n22b
-
-n100 : CNat
-n100   = cmul n10   n10
-
-n100b : CNat
-n100b  = cmul n10b  n10b
-
-n10k : CNat
-n10k   = cmul n100  n100
-
-n10kb : CNat
-n10kb  = cmul n100b n100b
-
-n100k : CNat
-n100k  = cmul n10k  n10
-
-n100kb : CNat
-n100kb = cmul n10kb n10b
-
-n1M : CNat
-n1M    = cmul n10k  n100
-
-n1Mb : CNat
-n1Mb   = cmul n10kb n100b
-
-n5M : CNat
-n5M    = cmul n1M   n5
-
-n5Mb : CNat
-n5Mb   = cmul n1Mb  n5
-
-n10M : CNat
-n10M   = cmul n5M   n2
-
-n10Mb : CNat
-n10Mb  = cmul n5Mb  n2
-
-Tree : Type
-Tree = (T : Type) -> (T -> T -> T) -> T -> T
-
-leaf : Tree
-leaf = \t, n, l => l
-
-node : Tree -> Tree -> Tree
-node = \t1, t2, t, n, l => n (t1 t n l) (t2 t n l)
-
-fullTree : CNat -> Tree
-fullTree = \n => n Tree (\t => node t t) leaf
-
--- full tree with given trees at bottom level
-fullTreeWithLeaf : Tree -> CNat -> Tree
-fullTreeWithLeaf = \bottom, n => n Tree (\t => node t t) bottom
-
-forceTree : Tree -> CBool
-forceTree = \t => t CBool and ctrue
-
-t15 : Tree
-t15  = fullTree n15
-t15b : Tree
-t15b = fullTree n15b
-t18 : Tree
-t18  = fullTree n18
-t18b : Tree
-t18b = fullTree n18b
-t19 : Tree
-t19  = fullTree n19
-t19b : Tree
-t19b = fullTree n19b
-t20 : Tree
-t20  = fullTree n20
-t20b : Tree
-t20b = fullTree n20b
-t21 : Tree
-t21  = fullTree n21
-t21b : Tree
-t21b = fullTree n21b
-t22 : Tree
-t22  = fullTree n22
-t22b : Tree
-t22b = fullTree n22b
-t23 : Tree
-t23  = fullTree n23
-t23b : Tree
-t23b = fullTree n23b
-
--- CNat conversion
---------------------------------------------------------------------------------
-
-convn1M : CEq Main.n1M Main.n1Mb
-convn1M = crefl
-
--- convn5M : CEq Main.n5M Main.n5Mb
--- convn5M = crefl
-
--- convn10M : CEq Main.n10M Main.n10Mb
--- convn10M = crefl
-
--- Full tree conversion
---------------------------------------------------------------------------------
-
--- convt15  : CEq Main.t15  Main.t15b
--- convt15  = crefl
--- convt18  : CEq Main.t18  Main.t18b
--- convt18  = crefl
--- convt19  : CEq Main.t19  Main.t19b
--- convt19  = crefl
--- convt20  : CEq Main.t20  Main.t20b
--- convt20  = crefl
--- convt21  : CEq Main.t21  Main.t21b
--- convt21  = crefl
--- convt22  : CEq Main.t22  Main.t22b
--- convt22  = crefl
--- convt23  : CEq Main.t23  Main.t23b
--- convt23  = crefl
-
--- Full meta-containing tree conversion
---------------------------------------------------------------------------------
-
--- convmt15 : CEq Main.t15b  (fullTreeWithLeaf ? Main.n15 )
--- convmt15 = crefl
--- convmt18 : CEq Main.t18b  (fullTreeWithLeaf ? Main.n18 )
--- convmt18 = crefl
--- convmt19 : CEq Main.t19b  (fullTreeWithLeaf ? Main.n19 )
--- convmt19 = crefl
--- convmt20 : CEq Main.t20b  (fullTreeWithLeaf ? Main.n20 )
--- convmt20 = crefl
--- convmt21 : CEq Main.t21b  (fullTreeWithLeaf ? Main.n21 )
--- convmt21 = crefl
--- convmt22 : CEq Main.t22b  (fullTreeWithLeaf ? Main.n22 )
--- convmt22 = crefl
--- convmt23 : CEq Main.t23b  (fullTreeWithLeaf ? Main.n23 )
--- convmt23 = crefl
-
--- Full tree forcing
---------------------------------------------------------------------------------
-
--- forcet15 : CEq (toBool (forceTree Main.t15)) True
--- forcet15 = crefl
--- forcet18 : CEq (toBool (forceTree Main.t18)) True
--- forcet18 = crefl
--- forcet19 : CEq (toBool (forceTree Main.t19)) True
--- forcet19 = crefl
--- forcet20 : CEq (toBool (forceTree Main.t20)) True
--- forcet20 = crefl
--- forcet21 : CEq (toBool (forceTree Main.t21)) True
--- forcet21 = crefl
---forcet22 : CEq (toBool (forceTree Main.t22)) True
---forcet22 = crefl
--- forcet23 : CEq (toBool (forceTree Main.t23)) True
--- forcet23 = crefl

bench/conv_eval.kind2

@@ -1,156 +0,0 @@
-Bool : Type
-True : Bool
-False : Bool
-
-CBool : Type
-CBool = (t: Type) t -> t -> t
-
-CBool.to_bool (x : CBool) : Bool
-CBool.to_bool x = (x Bool True False)
-
-CTrue : CBool
-CTrue = p => t => f => t
-
-CFalse : CBool
-CFalse = p => t => f => f
-
-And (a: CBool) (b: CBool) : CBool
-And a b = p => t => f => (a p (b p t f) f)
-
-CNat : Type
-CNat = (n: Type) (n -> n) -> n -> n
-
-Add (a: CNat) (b: CNat) : CNat
-Add a b = n => s => z => (a n s (b n s z))
-
-CMul (a: CNat) (b: CNat) : CNat
-CMul a b = n => s => (a n (b n s))
-
-Suc (a: CNat) : CNat
-Suc a = n => s => z => (s (a n s z))
-
-CEqual (t: Type) (a: t) (b: t) : Type
-CEqual t a b = (p: t -> Type) (p a) -> (p b)
-
-CRefl (t: Type) (x: t) : (CEqual t x x)
-CRefl t x = p => px => px
-
-N0 : CNat
-N0 = n => s => z => z
-
-N2 : CNat
-N2 = n => s => z => (s (s z))
-
-N3 : CNat
-N3 = n => s => z => (s (s (s z)))
-
-N4 : CNat
-N4 = n => s => z => (s (s (s (s z))))
-
-N5 : CNat
-N5 = n => s => z => (s (s (s (s (s z)))))
-
-N10 : CNat
-N10 = (CMul N2 N5)
-
-N10b : CNat
-N10b = (CMul N5 N2)
-
-N15 : CNat
-N15 = (Add N10 N5)
-
-N15b : CNat
-N15b = (Add N10b N5)
-
-N18 : CNat
-N18 = (Add N15 N3)
-
-N18b : CNat
-N18b = (Add N15b N3)
-
-N19 : CNat
-N19 = (Add N15 N4)
-
-N19b : CNat
-N19b = (Add N15b N4)
-
-N20 : CNat
-N20 = (CMul N2 N10)
-
-N20b : CNat
-N20b = (CMul N2 N10b)
-
-N21 : CNat
-N21 = (Suc N20)
-
-N21b : CNat
-N21b = (Suc N20b)
-
-N22 : CNat
-N22 = (Suc N21)
-
-N22b : CNat
-N22b = (Suc N21b)
-
-N23 : CNat
-N23 = (Suc N22)
-
-N23b : CNat
-N23b = (Suc N22b)
-
-N100 : CNat
-N100 = (CMul N10 N10)
-
-N100b : CNat
-N100b = (CMul N10b N10b)
-
-N10k : CNat
-N10k = (CMul N100 N100)
-
-N10kb : CNat
-N10kb = (CMul N100b N100b)
-
-N100k : CNat
-N100k = (CMul N10k N10)
-
-N100kb : CNat
-N100kb = (CMul N10kb N10b)
-
-N1M : CNat
-N1M = (CMul N10k N100)
-
-N1Mb : CNat
-N1Mb = (CMul N10kb N100b)
-
-N5M : CNat
-N5M = (CMul N1M N5)
-
-N5Mb : CNat
-N5Mb = (CMul N1Mb N5)
-
-N10M : CNat
-N10M = (CMul N5M N2)
-
-N10Mb : CNat
-N10Mb = (CMul N5Mb N2)
-
-CTree : Type
-CTree = (t: Type) (t -> t -> t) -> t -> t
-
-CLeaf : CTree
-CLeaf = t => n => l => l
-
-CNode (t1: CTree) (t2: CTree) : CTree
-CNode t1 t2 = t => n => l => (n (t1 t n l) (t2 t n l))
-
-FullCTree (n: CNat) : CTree
-FullCTree n = (n CTree (t => CNode t t) CLeaf)
-
-Num : CNat
-Num = N2
-
-Force (n: CNat) : Bool
-Force n = (n Bool (x => x) True)
-
-Main : (CEqual CNat N1M N1Mb)
-Main = (CRefl CNat N1M)

bench/nat_exp.agda

@@ -1,25 +0,0 @@
-data Nat : Set where
-  z : Nat
-  s : Nat -> Nat
-
-data The : (x : Nat) -> Set where
-  val : (x : Nat) -> The x
-
-add : Nat -> Nat -> Nat
-add a (s b) = s (add a b)
-add a z     = a
-
-mul : Nat -> Nat -> Nat
-mul a (s b) = add a (mul a b)
-mul a z     = z
-
-exp : Nat -> Nat -> Nat
-exp a (s b) = mul a (exp a b)
-exp a     z = s z
-
-nul : Nat -> Nat
-nul (s a) = (nul a)
-nul z     = z
-
-work : The (nul (exp (s (s (s z))) (s (s (s (s (s (s (s (s z))))))))))
-work = val z

bench/nat_exp.idr

@@ -1,26 +0,0 @@
-data NAT : Type where
-  Z : NAT
-  S : NAT -> NAT
-
-data The : NAT -> Type where
-  Val : (x : NAT) -> The x
-
-add : NAT -> NAT -> NAT
-add a (S b) = S (add a b)
-add a Z     = a
-
-mul : NAT -> NAT -> NAT
-mul a (S b) = add a (mul a b)
-mul a Z     = Z
-
-exp : NAT -> NAT -> NAT
-exp a (S b) = mul a (exp a b)
-exp a     Z = S Z
-
-nul : NAT -> NAT
-nul (S a) = nul a
-nul Z     = Z
-
-work : The (nul (exp (S (S (S Z))) (S (S (S (S (S (S (S (S Z))))))))))
-work = Val Z
-

bench/nat_exp.kind2

@@ -1,26 +0,0 @@
-Nat : Type
-Z : Nat
-S (pred: Nat) : Nat
-
-The (x: Nat) : Type
-Val (x: Nat) : (The x)
-
-Add (a: Nat) (b: Nat) : Nat
-Add a (S b) = (S (Add a b))
-Add a (Z)   = a
-
-Mul (a: Nat) (b: Nat) : Nat
-Mul a (S b) = (Add a (Mul a b))
-Mul a (Z)   = (Z)
-
-Exp (a: Nat) (b: Nat) : Nat
-Exp a (S b) = (Mul a (Exp a b))
-Exp a (Z)   = (S Z)
-
-Nul (n: Nat) : Nat
-Nul (S a) = (Nul a)
-Nul (Z)   = (Z)
-
-Work : (The (Nul (Exp (S (S (S Z))) (S (S (S (S (S (S (S (S Z))))))))))) {
-  (Val Z)
-}

bench/nat_exp.lean

@@ -1,25 +0,0 @@
-inductive NAT where
-  | Z : NAT
-  | S : NAT -> NAT
-
-inductive The : NAT -> Type where
-  | val : (x : NAT) -> The x
-
-def add : NAT -> NAT -> NAT
-  | a, NAT.S b => NAT.S (add a b)
-  | a, NAT.Z   => a
-
-def mul : NAT -> NAT -> NAT
-  | a, NAT.S b => add a (mul a b)
-  | _, NAT.Z   => NAT.Z
-
-def exp : NAT -> NAT -> NAT
-  | a, NAT.S b => mul a (exp a b)
-  | _, NAT.Z   => NAT.S NAT.Z
-
-def nul : NAT -> NAT
-  | NAT.S a => nul a
-  | NAT.Z   => NAT.Z
- 
-def work : The (nul (exp (NAT.S (NAT.S (NAT.S NAT.Z))) (NAT.S (NAT.S (NAT.S (NAT.S (NAT.S (NAT.S (NAT.S (NAT.S NAT.Z))))))))))
-  := @The.val NAT.Z

bench/nat_exp.v

@@ -1,36 +0,0 @@
-Inductive Nat : Type :=
-  | Z
-  | S : Nat -> Nat.
-
-(* Inductive The : Nat -> Type :=
-   | val : forall (x : Nat), The x. *)
-
-Inductive The : Nat -> Prop :=
-  | val (x : Nat) : The x.
-
-Fixpoint add (m : Nat) (n : Nat) : Nat :=
-  match m, n with
-  | m, Z     => m
-  | m, (S n) => S (add m n)
-  end.
-
-Fixpoint mul (m : Nat) (n : Nat) : Nat :=
-  match m, n with
-  | m, Z     => Z
-  | m, (S n) => (add m (mul m n))
-  end.
-
-Fixpoint exp (m : Nat) (n : Nat) : Nat :=
-  match m, n with
-  | m, Z     => (S Z)
-  | m, (S n) => (mul m (exp m n))
-  end.
-
-Fixpoint nul (n : Nat) : Nat :=
-  match n with
-  | Z     => Z
-  | (S n) => nul n
-  end.
-
-Definition work : The (nul (exp (S (S (S Z))) (S (S (S (S (S (S (S (S Z)))))))))) :=
-   val Z.

bootstrap.sh

@@ -13,8 +13,10 @@ echo "Building Kind2 type checker"
 
 # Probably we should just use git clone in Wikind?
 cd ../Wikind
-$KIND2 check Kind/TypeChecker.kind2
+#$KIND2 check Kind/TypeChecker.kind2
 $KIND2 to-hvm Kind/TypeChecker.kind2 > ../Kind2/src/checker.hvm
 
-cd $CURRENT
-cargo build --release
+cargo install --path $CURRENT
+
+#cd $CURRENT
+#cargo build --release

src/checker.hvm

@@ -9,6 +9,7 @@
 (Kind.Term.set_origin new_origin (Kind.Term.lam old_orig name body)) = (Kind.Term.lam new_origin name body)
 (Kind.Term.set_origin new_origin (Kind.Term.let old_orig name expr body)) = (Kind.Term.let new_origin name expr body)
 (Kind.Term.set_origin new_origin (Kind.Term.ann old_orig expr typ)) = (Kind.Term.ann new_origin expr typ)
+(Kind.Term.set_origin new_origin (Kind.Term.sub old_orig name indx redx expr)) = (Kind.Term.sub new_origin name indx redx expr)
 (Kind.Term.set_origin new_origin (Kind.Term.app old_orig func arg)) = (Kind.Term.app new_origin func arg)
 (Kind.Term.set_origin new_origin (Kind.Term.hlp old_orig)) = (Kind.Term.hlp new_origin)
 (Kind.Term.set_origin new_origin (Kind.Term.u60 old_orig)) = (Kind.Term.u60 new_origin)
@@ -36,28 +37,9 @@
 // Kind.API.check_all : (String)
 (Kind.API.check_all) = let output = (Kind.API.output (List.reverse (Kind.API.check_functions (Functions)))); (Bool.if (String.is_nil output) (Kind.Printer.text (List.cons "All terms check." (List.cons (String.new_line) (List.cons (String.new_line) (List.nil))))) output)
 
-// Bool.if -(a: Type) (b: (Bool)) (t: a) (f: a) : a
-(Bool.if (Bool.true) t f) = t
-(Bool.if (Bool.false) t f) = f
-
-// String.new_line : (String)
-(String.new_line) = (String.pure (Char.newline))
-
-// Char.newline : (Char)
-(Char.newline) = 10
-
-// Char : Type
-(Char) = 0
-
-// String.pure (x: (Char)) : (String)
-(String.pure x) = (String.cons x "")
-
-// List.reverse -(a: Type) (xs: (List a)) : (List a)
-(List.reverse xs) = (List.reverse.go xs (List.nil))
-
-// List.reverse.go -(a: Type) (xs: (List a)) (ys: (List a)) : (List a)
-(List.reverse.go (List.nil) ys) = ys
-(List.reverse.go (List.cons x xs) ys) = (List.reverse.go xs (List.cons x ys))
+// String.is_nil (xs: (String)) : (Bool)
+(String.is_nil "") = (Bool.true)
+(String.is_nil (String.cons x xs)) = (Bool.false)
 
 // Kind.API.output (res: (List (Pair U60 (List (Kind.Result (Unit)))))) : (String)
 (Kind.API.output (List.nil)) = ""
@@ -85,19 +67,20 @@
 // Kind.API.output.error.details (fnid: U60) (ctx: (Kind.Context)) (sub: (Kind.Subst)) (origin: U60) : (String)
 (Kind.API.output.error.details fnid ctx sub orig) = (Kind.Printer.text (List.cons (Bool.if (Kind.Context.is_empty ctx) "" (Kind.Printer.text (List.cons (Kind.Printer.color "4") (List.cons "Kind.Context:" (List.cons (Kind.Printer.color "0") (List.cons (String.new_line) (List.cons (Kind.Context.show ctx sub) (List.nil)))))))) (List.cons (Kind.Printer.color "4") (List.cons (String.cons 79 (String.cons 110 (String.cons 32 (String.cons 39 "{{#F")))) (List.cons (Show.to_string (U60.show (>> orig 48))) (List.cons (String.cons 70 (String.cons 35 (String.cons 125 (String.cons 125 (String.cons 39 ":"))))) (List.cons (Kind.Printer.color "0") (List.cons (String.new_line) (List.cons "{{#R" (List.cons (Show.to_string (U60.show (>> orig 48))) (List.cons ":" (List.cons (Show.to_string (U60.show (& orig 16777215))) (List.cons ":" (List.cons (Show.to_string (U60.show (& (>> orig 24) 16777215))) (List.cons "R#}}" (List.cons (String.new_line) (List.nil)))))))))))))))))
 
+// Pair.match -(a: Type) -(b: Type) (x: (Pair a b)) -(p: (x: (Pair a b)) Type) (new: (fst: a) (snd: b) (p (Pair.new a b fst snd))) : (p x)
+(Pair.match (Pair.new fst_ snd_) new) = ((new fst_) snd_)
+
+// Kind.Printer.text (ls: (List (String))) : (String)
+(Kind.Printer.text (List.nil)) = ""
+(Kind.Printer.text (List.cons x xs)) = (String.concat x (Kind.Printer.text xs))
+
+// String.concat (xs: (String)) (ys: (String)) : (String)
+(String.concat (String.cons x xs) ys) = (String.cons x (String.concat xs ys))
+(String.concat "" ys) = ys
+
 // Pair.fst -(a: Type) -(b: Type) (pair: (Pair a b)) : a
 (Pair.fst (Pair.new fst snd)) = fst
 
-// Kind.Context.is_empty (ctx: (Kind.Context)) : (Bool)
-(Kind.Context.is_empty (Kind.Context.empty)) = (Bool.true)
-(Kind.Context.is_empty (Kind.Context.entry name type vals rest)) = (Bool.false)
-
-// Show.to_string (show: (Show)) : (String)
-(Show.to_string show) = (show "")
-
-// Show : Type
-(Show) = 0
-
 // String.cut.go (str: (String)) (df: (String)) (n: U60) : (String)
 (String.cut.go "" df n) = ""
 (String.cut.go (String.cons x xs) df 0) = df
@@ -106,13 +89,9 @@
 // String.cut (str: (String)) : (String)
 (String.cut str) = (String.cut.go str "(...)" 2048)
 
-// U60.show (n: U60) : (Show)
-(U60.show 0) = @str (String.cons 48 str)
-(U60.show n) = @str let next = (String.cons (+ 48 (% n 10)) str); let func = (U60.if (< n 10) @h h @h ((U60.show (/ n 10)) h)); (func next)
-
-// U60.if -(r: Type) (n: U60) (t: r) (f: r) : r
-(U60.if 0 t f) = f
-(U60.if x t f) = t
+// Kind.Context.is_empty (ctx: (Kind.Context)) : (Bool)
+(Kind.Context.is_empty (Kind.Context.empty)) = (Bool.true)
+(Kind.Context.is_empty (Kind.Context.entry name type vals rest)) = (Bool.false)
 
 // Kind.Context.show.type (name: U60) (type: (Kind.Term)) (sub: (Kind.Subst)) (pad: U60) : (String)
 (Kind.Context.show.type name type sub pad) = (Kind.Printer.text (List.cons "- " (List.cons (String.pad_right (U60.to_nat pad) 32 (Kind.Name.show name)) (List.cons " : " (List.cons (String.cut (Kind.Term.show (Kind.Term.fill type sub))) (List.cons (String.new_line) (List.nil)))))))
@@ -128,12 +107,13 @@
 // Kind.Context.show (ctx: (Kind.Context)) (subst: (Kind.Subst)) : (String)
 (Kind.Context.show ctx subst) = (Kind.Context.show.go ctx subst (Kind.Context.max_name_length ctx))
 
-// Kind.Context.max_name_length.aux (ctx: (Kind.Context)) (acc: U60) : U60
-(Kind.Context.max_name_length.aux (Kind.Context.empty) acc) = acc
-(Kind.Context.max_name_length.aux (Kind.Context.entry name type vals rest) acc) = (Kind.Context.max_name_length.aux rest (U60.max (Nat.to_u60 (String.length (Kind.Name.show name))) acc))
+// String.pad_right (size: (Nat)) (chr: (Char)) (str: (String)) : (String)
+(String.pad_right (Nat.zero) chr str) = str
+(String.pad_right (Nat.succ sp) chr "") = (String.cons chr (String.pad_right sp chr ""))
+(String.pad_right (Nat.succ sp) chr (String.cons x xs)) = (String.cons x (String.pad_right sp chr xs))
 
-// Kind.Context.max_name_length (ctx: (Kind.Context)) : U60
-(Kind.Context.max_name_length ctx) = (Kind.Context.max_name_length.aux ctx 0)
+// Char : Type
+(Char) = 0
 
 // Kind.Name.show.go (name: U60) (chrs: (String)) : (String)
 (Kind.Name.show.go name chrs) = (U60.if (== name 0) chrs let val = (% name 64); let chr = (U60.if (== val 0) 46 (U60.if (& (<= 1 val) (<= val 10)) (+ (- val 1) 48) (U60.if (& (<= 11 val) (<= val 36)) (+ (- val 11) 65) (U60.if (& (<= 37 val) (<= val 62)) (+ (- val 37) 97) (U60.if (== val 63) 95 63))))); (Kind.Name.show.go (/ name 64) (String.cons chr chrs)))
@@ -141,16 +121,134 @@
 // Kind.Name.show (name: U60) : (String)
 (Kind.Name.show name) = (Kind.Name.show.go name "")
 
-// U60.max (fst: U60) (snd: U60) : U60
-(U60.max fst snd) = (U60.if (> fst snd) fst snd)
+// U60.if -(r: Type) (n: U60) (t: r) (f: r) : r
+(U60.if 0 t f) = f
+(U60.if x t f) = t
 
-// Nat.to_u60 (n: (Nat)) : U60
-(Nat.to_u60 (Nat.zero)) = 0
-(Nat.to_u60 (Nat.succ n)) = (+ 1 (Nat.to_u60 n))
+// Kind.Term.show.forall (orig: U60) (name: U60) (type: (Kind.Term)) (body: (_: (Kind.Term)) (Kind.Term)) : (String)
+(Kind.Term.show.forall orig name type body) = (U60.if (== name 63) (Kind.Printer.text (List.cons "(" (List.cons (Kind.Term.show type) (List.cons " -> " (List.cons (Kind.Term.show (body (Kind.Term.var orig name 0))) (List.cons ")" (List.nil))))))) (Kind.Printer.text (List.cons "((" (List.cons (Kind.Name.show name) (List.cons ": " (List.cons (Kind.Term.show type) (List.cons ") -> " (List.cons (Kind.Term.show (body (Kind.Term.var orig name 0))) (List.cons ")" (List.nil))))))))))
 
-// String.length (xs: (String)) : (Nat)
-(String.length "") = (Nat.zero)
-(String.length (String.cons x xs)) = (Nat.succ (String.length xs))
+// Kind.Term.show (term: (Kind.Term)) : (String)
+(Kind.Term.show term) = let sugars = (List.cons (Kind.Term.show.sugar.string term) (List.cons (Kind.Term.show.sugar.list term) (List.cons (Kind.Term.show.sugar.sigma term) (List.nil)))); (Maybe.try sugars (Kind.Term.show.go term))
+
+// Kind.Term.show.go (term: (Kind.Term)) : (String)
+(Kind.Term.show.go (Kind.Term.typ orig)) = "Type"
+(Kind.Term.show.go (Kind.Term.var orig name index)) = (Kind.Printer.text (List.cons (Kind.Name.show name) (List.nil)))
+(Kind.Term.show.go (Kind.Term.hol orig numb)) = (Kind.Printer.text (List.cons "_" (List.nil)))
+(Kind.Term.show.go (Kind.Term.all orig name type body)) = (Kind.Term.show.forall orig name type body)
+(Kind.Term.show.go (Kind.Term.lam orig name body)) = (Kind.Printer.text (List.cons "(" (List.cons (Kind.Name.show name) (List.cons " => " (List.cons (Kind.Term.show (body (Kind.Term.var orig name 0))) (List.cons ")" (List.nil)))))))
+(Kind.Term.show.go (Kind.Term.let orig name exp body)) = (Kind.Printer.text (List.cons "let " (List.cons (Kind.Name.show name) (List.cons " = " (List.cons (Kind.Term.show exp) (List.cons "; " (List.cons (Kind.Term.show (body (Kind.Term.var orig name 0))) (List.nil))))))))
+(Kind.Term.show.go (Kind.Term.ann orig expr type)) = (Kind.Printer.text (List.cons "{" (List.cons (Kind.Term.show expr) (List.cons " :: " (List.cons (Kind.Term.show type) (List.cons "}" (List.nil)))))))
+(Kind.Term.show.go (Kind.Term.sub orig name indx redx expr)) = (Kind.Printer.text (List.cons (Kind.Term.show expr) (List.cons " ## " (List.cons (Kind.Name.show name) (List.cons "/" (List.cons (Show.to_string (U60.show redx)) (List.nil)))))))
+(Kind.Term.show.go (Kind.Term.app orig func argm)) = (Kind.Printer.text (List.cons "(" (List.cons (Kind.Term.show func) (List.cons " " (List.cons (Kind.Term.show argm) (List.cons ")" (List.nil)))))))
+(Kind.Term.show.go (Kind.Term.ct0 ctid orig)) = (NameOf ctid)
+(Kind.Term.show.go (Kind.Term.ct1 ctid orig x0)) = (Kind.Printer.text (List.cons "(" (List.cons (NameOf ctid) (List.cons " " (List.cons (Kind.Term.show x0) (List.cons ")" (List.nil)))))))
+(Kind.Term.show.go (Kind.Term.ct2 ctid orig x0 x1)) = (Kind.Printer.text (List.cons "(" (List.cons (NameOf ctid) (List.cons " " (List.cons (Kind.Term.show x0) (List.cons " " (List.cons (Kind.Term.show x1) (List.cons ")" (List.nil)))))))))
+(Kind.Term.show.go (Kind.Term.ct3 ctid orig x0 x1 x2)) = (Kind.Printer.text (List.cons "(" (List.cons (NameOf ctid) (List.cons " " (List.cons (Kind.Term.show x0) (List.cons " " (List.cons (Kind.Term.show x1) (List.cons " " (List.cons (Kind.Term.show x2) (List.cons ")" (List.nil)))))))))))
+(Kind.Term.show.go (Kind.Term.ct4 ctid orig x0 x1 x2 x3)) = (Kind.Printer.text (List.cons "(" (List.cons (NameOf ctid) (List.cons " " (List.cons (Kind.Term.show x0) (List.cons " " (List.cons (Kind.Term.show x1) (List.cons " " (List.cons (Kind.Term.show x2) (List.cons " " (List.cons (Kind.Term.show x3) (List.cons ")" (List.nil)))))))))))))
+(Kind.Term.show.go (Kind.Term.ct5 ctid orig x0 x1 x2 x3 x4)) = (Kind.Printer.text (List.cons "(" (List.cons (NameOf ctid) (List.cons " " (List.cons (Kind.Term.show x0) (List.cons " " (List.cons (Kind.Term.show x1) (List.cons " " (List.cons (Kind.Term.show x2) (List.cons " " (List.cons (Kind.Term.show x3) (List.cons " " (List.cons (Kind.Term.show x4) (List.cons ")" (List.nil)))))))))))))))
+(Kind.Term.show.go (Kind.Term.ct6 ctid orig x0 x1 x2 x3 x4 x5)) = (Kind.Printer.text (List.cons "(" (List.cons (NameOf ctid) (List.cons " " (List.cons (Kind.Term.show x0) (List.cons " " (List.cons (Kind.Term.show x1) (List.cons " " (List.cons (Kind.Term.show x2) (List.cons " " (List.cons (Kind.Term.show x3) (List.cons " " (List.cons (Kind.Term.show x4) (List.cons " " (List.cons (Kind.Term.show x5) (List.cons ")" (List.nil)))))))))))))))))
+(Kind.Term.show.go (Kind.Term.ct7 ctid orig args)) = (Kind.Printer.text (List.cons "(" (List.cons (NameOf ctid) (List.cons " " (List.cons (Kind.Term.show args) (List.cons ")" (List.nil)))))))
+(Kind.Term.show.go (Kind.Term.ct8 ctid orig args)) = (Kind.Printer.text (List.cons "(" (List.cons (NameOf ctid) (List.cons " " (List.cons (Kind.Term.show args) (List.cons ")" (List.nil)))))))
+(Kind.Term.show.go (Kind.Term.fn0 ctid orig)) = (NameOf ctid)
+(Kind.Term.show.go (Kind.Term.fn1 ctid orig x0)) = (Kind.Printer.text (List.cons "(" (List.cons (NameOf ctid) (List.cons " " (List.cons (Kind.Term.show x0) (List.cons ")" (List.nil)))))))
+(Kind.Term.show.go (Kind.Term.fn2 ctid orig x0 x1)) = (Kind.Printer.text (List.cons "(" (List.cons (NameOf ctid) (List.cons " " (List.cons (Kind.Term.show x0) (List.cons " " (List.cons (Kind.Term.show x1) (List.cons ")" (List.nil)))))))))
+(Kind.Term.show.go (Kind.Term.fn3 ctid orig x0 x1 x2)) = (Kind.Printer.text (List.cons "(" (List.cons (NameOf ctid) (List.cons " " (List.cons (Kind.Term.show x0) (List.cons " " (List.cons (Kind.Term.show x1) (List.cons " " (List.cons (Kind.Term.show x2) (List.cons ")" (List.nil)))))))))))
+(Kind.Term.show.go (Kind.Term.fn4 ctid orig x0 x1 x2 x3)) = (Kind.Printer.text (List.cons "(" (List.cons (NameOf ctid) (List.cons " " (List.cons (Kind.Term.show x0) (List.cons " " (List.cons (Kind.Term.show x1) (List.cons " " (List.cons (Kind.Term.show x2) (List.cons " " (List.cons (Kind.Term.show x3) (List.cons ")" (List.nil)))))))))))))
+(Kind.Term.show.go (Kind.Term.fn5 ctid orig x0 x1 x2 x3 x4)) = (Kind.Printer.text (List.cons "(" (List.cons (NameOf ctid) (List.cons " " (List.cons (Kind.Term.show x0) (List.cons " " (List.cons (Kind.Term.show x1) (List.cons " " (List.cons (Kind.Term.show x2) (List.cons " " (List.cons (Kind.Term.show x3) (List.cons " " (List.cons (Kind.Term.show x4) (List.cons ")" (List.nil)))))))))))))))
+(Kind.Term.show.go (Kind.Term.fn6 ctid orig x0 x1 x2 x3 x4 x5)) = (Kind.Printer.text (List.cons "(" (List.cons (NameOf ctid) (List.cons " " (List.cons (Kind.Term.show x0) (List.cons " " (List.cons (Kind.Term.show x1) (List.cons " " (List.cons (Kind.Term.show x2) (List.cons " " (List.cons (Kind.Term.show x3) (List.cons " " (List.cons (Kind.Term.show x4) (List.cons " " (List.cons (Kind.Term.show x5) (List.cons ")" (List.nil)))))))))))))))))
+(Kind.Term.show.go (Kind.Term.fn7 ctid orig args)) = (Kind.Printer.text (List.cons "(" (List.cons (NameOf ctid) (List.cons " " (List.cons (Kind.Term.show args) (List.cons ")" (List.nil)))))))
+(Kind.Term.show.go (Kind.Term.fn8 ctid orig args)) = (Kind.Printer.text (List.cons "(" (List.cons (NameOf ctid) (List.cons " " (List.cons (Kind.Term.show args) (List.cons ")" (List.nil)))))))
+(Kind.Term.show.go (Kind.Term.args7 x0 x1 x2 x3 x4 x5 x6)) = (Kind.Printer.text (List.cons (Kind.Term.show x0) (List.cons " " (List.cons (Kind.Term.show x1) (List.cons " " (List.cons (Kind.Term.show x2) (List.cons " " (List.cons (Kind.Term.show x3) (List.cons " " (List.cons (Kind.Term.show x4) (List.cons " " (List.cons (Kind.Term.show x5) (List.cons " " (List.cons (Kind.Term.show x6) (List.nil)))))))))))))))
+(Kind.Term.show.go (Kind.Term.args8 x0 x1 x2 x3 x4 x5 x6 x7)) = (Kind.Printer.text (List.cons (Kind.Term.show x0) (List.cons " " (List.cons (Kind.Term.show x1) (List.cons " " (List.cons (Kind.Term.show x2) (List.cons " " (List.cons (Kind.Term.show x3) (List.cons " " (List.cons (Kind.Term.show x4) (List.cons " " (List.cons (Kind.Term.show x5) (List.cons " " (List.cons (Kind.Term.show x6) (List.cons " " (List.cons (Kind.Term.show x7) (List.nil)))))))))))))))))
+(Kind.Term.show.go (Kind.Term.hlp orig)) = "?"
+(Kind.Term.show.go (Kind.Term.u60 orig)) = "U60"
+(Kind.Term.show.go (Kind.Term.num orig numb)) = (Show.to_string (U60.show numb))
+(Kind.Term.show.go (Kind.Term.op2 orig operator left right)) = (Kind.Printer.text (List.cons "(" (List.cons (Kind.Operator.show operator) (List.cons " " (List.cons (Kind.Term.show left) (List.cons " " (List.cons (Kind.Term.show right) (List.cons ")" (List.nil)))))))))
+
+// Maybe.try -(a: Type) (ls: (List (Maybe a))) (alt: a) : a
+(Maybe.try (List.nil) alt) = alt
+(Maybe.try (List.cons maybe xs) alt) = (Maybe.match maybe (Maybe.try xs alt) @maybe.value maybe.value)
+
+// Maybe.match -(t: Type) (x: (Maybe t)) -(p: (x: (Maybe t)) Type) (none: (p (Maybe.none t))) (some: (value: t) (p (Maybe.some t value))) : (p x)
+(Maybe.match (Maybe.none) none some) = none
+(Maybe.match (Maybe.some value_) none some) = (some value_)
+
+// Kind.Term.show.sugar.list.go (term: (Kind.Term)) : (Maybe (List (String)))
+(Kind.Term.show.sugar.list.go (Kind.Term.ct0 (List.nil.) orig)) = (Maybe.some (List.nil))
+(Kind.Term.show.sugar.list.go (Kind.Term.ct2 (List.cons.) orig x0 x1)) = (Maybe.bind (Kind.Term.show.sugar.list.go x1) @tail (Maybe.pure (List.cons (Kind.Term.show x0) tail)))
+(Kind.Term.show.sugar.list.go other) = (Maybe.none)
+
+// Kind.Term.show.sugar.list (term: (Kind.Term)) : (Maybe (String))
+(Kind.Term.show.sugar.list term) = (Maybe.bind (Kind.Term.show.sugar.list.go term) @res (Maybe.pure (Kind.Printer.text (List.cons "[" (List.cons (String.join " " res) (List.cons "]" (List.nil)))))))
+
+// Maybe.bind -(a: Type) -(b: Type) (ma: (Maybe a)) (mb: (_: a) (Maybe b)) : (Maybe b)
+(Maybe.bind (Maybe.none) mb) = (Maybe.none)
+(Maybe.bind (Maybe.some val) mb) = (mb val)
+
+// Maybe.pure -(a: Type) (x: a) : (Maybe a)
+(Maybe.pure x) = (Maybe.some x)
+
+// String.join (sep: (String)) (list: (List (String))) : (String)
+(String.join sep list) = (String.intercalate sep list)
+
+// String.intercalate (sep: (String)) (xs: (List (String))) : (String)
+(String.intercalate sep xs) = (String.flatten (List.intersperse sep xs))
+
+// String.flatten (xs: (List (String))) : (String)
+(String.flatten (List.nil)) = ""
+(String.flatten (List.cons head tail)) = (String.concat head (String.flatten tail))
+
+// List.intersperse -(a: Type) (sep: a) (xs: (List a)) : (List a)
+(List.intersperse sep (List.nil)) = (List.nil)
+(List.intersperse sep (List.cons xh (List.nil))) = (List.pure xh)
+(List.intersperse sep (List.cons xh xt)) = (List.cons xh (List.cons sep (List.intersperse sep xt)))
+
+// List.pure -(t: Type) (x: t) : (List t)
+(List.pure x) = (List.cons x (List.nil))
+
+// Kind.Operator.show (op: (Kind.Operator)) : (String)
+(Kind.Operator.show (Kind.Operator.add)) = "+"
+(Kind.Operator.show (Kind.Operator.sub)) = "-"
+(Kind.Operator.show (Kind.Operator.mul)) = "*"
+(Kind.Operator.show (Kind.Operator.div)) = "/"
+(Kind.Operator.show (Kind.Operator.mod)) = "%"
+(Kind.Operator.show (Kind.Operator.and)) = "&"
+(Kind.Operator.show (Kind.Operator.or)) = "|"
+(Kind.Operator.show (Kind.Operator.xor)) = "^"
+(Kind.Operator.show (Kind.Operator.shl)) = "<<"
+(Kind.Operator.show (Kind.Operator.shr)) = ">>"
+(Kind.Operator.show (Kind.Operator.ltn)) = "<"
+(Kind.Operator.show (Kind.Operator.lte)) = "<="
+(Kind.Operator.show (Kind.Operator.eql)) = "=="
+(Kind.Operator.show (Kind.Operator.gte)) = ">="
+(Kind.Operator.show (Kind.Operator.gtn)) = ">"
+(Kind.Operator.show (Kind.Operator.neq)) = "!="
+
+// Kind.Term.show.sugar.string.go (term: (Kind.Term)) : (Maybe (String))
+(Kind.Term.show.sugar.string.go (Kind.Term.ct0 (String.nil.) orig)) = (Maybe.some "")
+(Kind.Term.show.sugar.string.go (Kind.Term.ct2 (String.cons.) orig (Kind.Term.num orig1 x0) x1)) = (Maybe.bind (Kind.Term.show.sugar.string.go x1) @tail (Maybe.pure (String.cons x0 tail)))
+(Kind.Term.show.sugar.string.go other) = (Maybe.none)
+
+// Kind.Term.show.sugar.string (term: (Kind.Term)) : (Maybe (String))
+(Kind.Term.show.sugar.string term) = (Maybe.bind (Kind.Term.show.sugar.string.go term) @res let quot = (String.cons 39 ""); (Maybe.pure (Kind.Printer.text (List.cons quot (List.cons res (List.cons quot (List.nil)))))))
+
+// U60.show (n: U60) : (Show)
+(U60.show 0) = @str (String.cons 48 str)
+(U60.show n) = @str let next = (String.cons (+ 48 (% n 10)) str); let func = (U60.if (< n 10) @h h @h ((U60.show (/ n 10)) h)); (func next)
+
+// Show : Type
+(Show) = 0
+
+// Kind.Term.show.sugar.sigma (term: (Kind.Term)) : (Maybe (String))
+(Kind.Term.show.sugar.sigma (Kind.Term.ct2 (Sigma.) orig typ (Kind.Term.lam orig_ name body))) = (Maybe.some (Kind.Printer.text (List.cons "([" (List.cons (Kind.Name.show name) (List.cons ": " (List.cons (Kind.Term.show typ) (List.cons "] -> " (List.cons (Kind.Term.show (body (Kind.Term.var orig_ name 0))) (List.cons ")" (List.nil))))))))))
+(Kind.Term.show.sugar.sigma term) = (Maybe.none)
+
+// Show.to_string (show: (Show)) : (String)
+(Show.to_string show) = (show "")
+
+// Show : Type
+(Show) = 0
 
 // Kind.Term.fill (term: (Kind.Term)) (subst: (Kind.Subst)) : (Kind.Term)
 (Kind.Term.fill term (Kind.Subst.end)) = term
@@ -160,6 +258,7 @@
 (Kind.Term.fill (Kind.Term.lam orig name body) sub) = (Kind.Term.lam orig name @x (Kind.Term.fill (body x) sub))
 (Kind.Term.fill (Kind.Term.let orig name expr body) sub) = (Kind.Term.eval_let orig name (Kind.Term.fill expr sub) @x (Kind.Term.fill (body x) sub))
 (Kind.Term.fill (Kind.Term.ann orig expr typ) sub) = (Kind.Term.eval_ann orig (Kind.Term.fill expr sub) (Kind.Term.fill typ sub))
+(Kind.Term.fill (Kind.Term.sub orig name indx redx expr) sub) = (Kind.Term.eval_sub orig name indx redx (Kind.Term.fill expr sub))
 (Kind.Term.fill (Kind.Term.app orig expr typ) sub) = (Kind.Term.eval_app orig (Kind.Term.fill expr sub) (Kind.Term.fill typ sub))
 (Kind.Term.fill (Kind.Term.hlp orig) sub) = (Kind.Term.hlp orig)
 (Kind.Term.fill (Kind.Term.u60 orig) sub) = (Kind.Term.u60 orig)
@@ -187,11 +286,9 @@
 (Kind.Term.fill (Kind.Term.args8 x0 x1 x2 x3 x4 x5 x6 x7) sub) = (Kind.Term.args8 (Kind.Term.fill x0 sub) (Kind.Term.fill x1 sub) (Kind.Term.fill x2 sub) (Kind.Term.fill x3 sub) (Kind.Term.fill x4 sub) (Kind.Term.fill x5 sub) (Kind.Term.fill x6 sub) (Kind.Term.fill x7 sub))
 (Kind.Term.fill (Kind.Term.hol orig numb) sub) = let substRes = (Kind.Subst.look sub numb); (Maybe.match substRes (Kind.Term.hol orig numb) @substRes.value (Kind.Term.fill substRes.value sub))
 
-// Kind.Term.eval_ann (orig: U60) (expr: (Kind.Term)) (type: (Kind.Term)) : (Kind.Term)
-(Kind.Term.eval_ann orig expr type) = expr
-
-// Kind.Term.eval_let (orig: U60) (name: U60) (expr: (Kind.Term)) (body: (_: (Kind.Term)) (Kind.Term)) : (Kind.Term)
-(Kind.Term.eval_let orig name expr body) = (body expr)
+// Kind.Term.eval_app (orig: U60) (left: (Kind.Term)) (right: (Kind.Term)) : (Kind.Term)
+(Kind.Term.eval_app orig (Kind.Term.lam orig1 name body) arg) = (body arg)
+(Kind.Term.eval_app orig func arg) = (Kind.Term.app orig func arg)
 
 // Kind.Subst.look (subst: (Kind.Subst)) (depth: U60) : (Maybe (Kind.Term))
 (Kind.Subst.look (Kind.Subst.end) 0) = (Maybe.none)
@@ -201,146 +298,62 @@
 (Kind.Subst.look (Kind.Subst.unfilled rest) n) = (Kind.Subst.look rest (- n 1))
 (Kind.Subst.look (Kind.Subst.sub term rest) n) = (Kind.Subst.look rest (- n 1))
 
-// Kind.Term.eval_app (orig: U60) (left: (Kind.Term)) (right: (Kind.Term)) : (Kind.Term)
-(Kind.Term.eval_app orig (Kind.Term.lam orig1 name body) arg) = (body arg)
-(Kind.Term.eval_app orig func arg) = (Kind.Term.app orig func arg)
+// Kind.Term.eval_ann (orig: U60) (expr: (Kind.Term)) (type: (Kind.Term)) : (Kind.Term)
+(Kind.Term.eval_ann orig expr type) = expr
 
-// Maybe.match -(t: Type) (x: (Maybe t)) -(p: (x: (Maybe t)) Type) (none: (p (Maybe.none t))) (some: (value: t) (p (Maybe.some t value))) : (p x)
-(Maybe.match (Maybe.none) none some) = none
-(Maybe.match (Maybe.some value_) none some) = (some value_)
+// Kind.Term.eval_let (orig: U60) (name: U60) (expr: (Kind.Term)) (body: (_: (Kind.Term)) (Kind.Term)) : (Kind.Term)
+(Kind.Term.eval_let orig name expr body) = (body expr)
+
+// Kind.Term.eval_sub (orig: U60) (name: U60) (indx: U60) (redx: U60) (expr: (Kind.Term)) : (Kind.Term)
+(Kind.Term.eval_sub orig name indx redx expr) = expr
+
+// Kind.Context.max_name_length.aux (ctx: (Kind.Context)) (acc: U60) : U60
+(Kind.Context.max_name_length.aux (Kind.Context.empty) acc) = acc
+(Kind.Context.max_name_length.aux (Kind.Context.entry name type vals rest) acc) = (Kind.Context.max_name_length.aux rest (U60.max (Nat.to_u60 (String.length (Kind.Name.show name))) acc))
+
+// Kind.Context.max_name_length (ctx: (Kind.Context)) : U60
+(Kind.Context.max_name_length ctx) = (Kind.Context.max_name_length.aux ctx 0)
+
+// U60.max (fst: U60) (snd: U60) : U60
+(U60.max fst snd) = (U60.if (> fst snd) fst snd)
+
+// String.length (xs: (String)) : (Nat)
+(String.length "") = (Nat.zero)
+(String.length (String.cons x xs)) = (Nat.succ (String.length xs))
+
+// Nat.to_u60 (n: (Nat)) : U60
+(Nat.to_u60 (Nat.zero)) = 0
+(Nat.to_u60 (Nat.succ n)) = (+ 1 (Nat.to_u60 n))
+
+// Kind.Printer.color (color_code: (String)) : (String)
+(Kind.Printer.color color_code) = (Kind.Printer.text (List.cons (String.cons 27 "") (List.cons "[" (List.cons color_code (List.cons "m" (List.nil))))))
+
+// String.new_line : (String)
+(String.new_line) = (String.pure (Char.newline))
+
+// String.pure (x: (Char)) : (String)
+(String.pure x) = (String.cons x "")
+
+// Char.newline : (Char)
+(Char.newline) = 10
 
 // U60.to_nat (x: U60) : (Nat)
 (U60.to_nat 0) = (Nat.zero)
 (U60.to_nat n) = (Nat.succ (U60.to_nat (- n 1)))
 
-// Kind.Printer.color (color_code: (String)) : (String)
-(Kind.Printer.color color_code) = (Kind.Printer.text (List.cons (String.cons 27 "") (List.cons "[" (List.cons color_code (List.cons "m" (List.nil))))))
-
-// Kind.Printer.text (ls: (List (String))) : (String)
-(Kind.Printer.text (List.nil)) = ""
-(Kind.Printer.text (List.cons x xs)) = (String.concat x (Kind.Printer.text xs))
-
-// String.concat (xs: (String)) (ys: (String)) : (String)
-(String.concat (String.cons x xs) ys) = (String.cons x (String.concat xs ys))
-(String.concat "" ys) = ys
-
-// Kind.Term.show.forall (orig: U60) (name: U60) (type: (Kind.Term)) (body: (_: (Kind.Term)) (Kind.Term)) : (String)
-(Kind.Term.show.forall orig name type body) = (U60.if (== name 63) (Kind.Printer.text (List.cons "(" (List.cons (Kind.Term.show type) (List.cons " -> " (List.cons (Kind.Term.show (body (Kind.Term.var orig name 0))) (List.cons ")" (List.nil))))))) (Kind.Printer.text (List.cons "((" (List.cons (Kind.Name.show name) (List.cons ": " (List.cons (Kind.Term.show type) (List.cons ") -> " (List.cons (Kind.Term.show (body (Kind.Term.var orig name 0))) (List.cons ")" (List.nil))))))))))
-
-// Kind.Term.show (term: (Kind.Term)) : (String)
-(Kind.Term.show term) = let sugars = (List.cons (Kind.Term.show.sugar.string term) (List.cons (Kind.Term.show.sugar.list term) (List.cons (Kind.Term.show.sugar.sigma term) (List.nil)))); (Maybe.try sugars (Kind.Term.show.go term))
-
-// Kind.Term.show.go (term: (Kind.Term)) : (String)
-(Kind.Term.show.go (Kind.Term.typ orig)) = "Type"
-(Kind.Term.show.go (Kind.Term.var orig name index)) = (Kind.Printer.text (List.cons (Kind.Name.show name) (List.nil)))
-(Kind.Term.show.go (Kind.Term.hol orig numb)) = (Kind.Printer.text (List.cons "_" (List.nil)))
-(Kind.Term.show.go (Kind.Term.all orig name type body)) = (Kind.Term.show.forall orig name type body)
-(Kind.Term.show.go (Kind.Term.lam orig name body)) = (Kind.Printer.text (List.cons "(" (List.cons (Kind.Name.show name) (List.cons "=>" (List.cons (Kind.Term.show (body (Kind.Term.var orig name 0))) (List.cons ")" (List.nil)))))))
-(Kind.Term.show.go (Kind.Term.let orig name exp body)) = (Kind.Printer.text (List.cons "let " (List.cons (Kind.Name.show name) (List.cons " = " (List.cons (Kind.Term.show exp) (List.cons "; " (List.cons (Kind.Term.show (body (Kind.Term.var orig name 0))) (List.nil))))))))
-(Kind.Term.show.go (Kind.Term.ann orig expr type)) = (Kind.Printer.text (List.cons "{" (List.cons (Kind.Term.show expr) (List.cons " :: " (List.cons (Kind.Term.show type) (List.cons "}" (List.nil)))))))
-(Kind.Term.show.go (Kind.Term.app orig func argm)) = (Kind.Printer.text (List.cons "(" (List.cons (Kind.Term.show func) (List.cons " " (List.cons (Kind.Term.show argm) (List.cons ")" (List.nil)))))))
-(Kind.Term.show.go (Kind.Term.ct0 ctid orig)) = (NameOf ctid)
-(Kind.Term.show.go (Kind.Term.ct1 ctid orig x0)) = (Kind.Printer.text (List.cons "(" (List.cons (NameOf ctid) (List.cons " " (List.cons (Kind.Term.show x0) (List.cons ")" (List.nil)))))))
-(Kind.Term.show.go (Kind.Term.ct2 ctid orig x0 x1)) = (Kind.Printer.text (List.cons "(" (List.cons (NameOf ctid) (List.cons " " (List.cons (Kind.Term.show x0) (List.cons " " (List.cons (Kind.Term.show x1) (List.cons ")" (List.nil)))))))))
-(Kind.Term.show.go (Kind.Term.ct3 ctid orig x0 x1 x2)) = (Kind.Printer.text (List.cons "(" (List.cons (NameOf ctid) (List.cons " " (List.cons (Kind.Term.show x0) (List.cons " " (List.cons (Kind.Term.show x1) (List.cons " " (List.cons (Kind.Term.show x2) (List.cons ")" (List.nil)))))))))))
-(Kind.Term.show.go (Kind.Term.ct4 ctid orig x0 x1 x2 x3)) = (Kind.Printer.text (List.cons "(" (List.cons (NameOf ctid) (List.cons " " (List.cons (Kind.Term.show x0) (List.cons " " (List.cons (Kind.Term.show x1) (List.cons " " (List.cons (Kind.Term.show x2) (List.cons " " (List.cons (Kind.Term.show x3) (List.cons ")" (List.nil)))))))))))))
-(Kind.Term.show.go (Kind.Term.ct5 ctid orig x0 x1 x2 x3 x4)) = (Kind.Printer.text (List.cons "(" (List.cons (NameOf ctid) (List.cons " " (List.cons (Kind.Term.show x0) (List.cons " " (List.cons (Kind.Term.show x1) (List.cons " " (List.cons (Kind.Term.show x2) (List.cons " " (List.cons (Kind.Term.show x3) (List.cons " " (List.cons (Kind.Term.show x4) (List.cons ")" (List.nil)))))))))))))))
-(Kind.Term.show.go (Kind.Term.ct6 ctid orig x0 x1 x2 x3 x4 x5)) = (Kind.Printer.text (List.cons "(" (List.cons (NameOf ctid) (List.cons " " (List.cons (Kind.Term.show x0) (List.cons " " (List.cons (Kind.Term.show x1) (List.cons " " (List.cons (Kind.Term.show x2) (List.cons " " (List.cons (Kind.Term.show x3) (List.cons " " (List.cons (Kind.Term.show x4) (List.cons " " (List.cons (Kind.Term.show x5) (List.cons ")" (List.nil)))))))))))))))))
-(Kind.Term.show.go (Kind.Term.ct7 ctid orig args)) = (Kind.Printer.text (List.cons "(" (List.cons (NameOf ctid) (List.cons " " (List.cons (Kind.Term.show args) (List.cons ")" (List.nil)))))))
-(Kind.Term.show.go (Kind.Term.ct8 ctid orig args)) = (Kind.Printer.text (List.cons "(" (List.cons (NameOf ctid) (List.cons " " (List.cons (Kind.Term.show args) (List.cons ")" (List.nil)))))))
-(Kind.Term.show.go (Kind.Term.fn0 ctid orig)) = (NameOf ctid)
-(Kind.Term.show.go (Kind.Term.fn1 ctid orig x0)) = (Kind.Printer.text (List.cons "(" (List.cons (NameOf ctid) (List.cons " " (List.cons (Kind.Term.show x0) (List.cons ")" (List.nil)))))))
-(Kind.Term.show.go (Kind.Term.fn2 ctid orig x0 x1)) = (Kind.Printer.text (List.cons "(" (List.cons (NameOf ctid) (List.cons " " (List.cons (Kind.Term.show x0) (List.cons " " (List.cons (Kind.Term.show x1) (List.cons ")" (List.nil)))))))))
-(Kind.Term.show.go (Kind.Term.fn3 ctid orig x0 x1 x2)) = (Kind.Printer.text (List.cons "(" (List.cons (NameOf ctid) (List.cons " " (List.cons (Kind.Term.show x0) (List.cons " " (List.cons (Kind.Term.show x1) (List.cons " " (List.cons (Kind.Term.show x2) (List.cons ")" (List.nil)))))))))))
-(Kind.Term.show.go (Kind.Term.fn4 ctid orig x0 x1 x2 x3)) = (Kind.Printer.text (List.cons "(" (List.cons (NameOf ctid) (List.cons " " (List.cons (Kind.Term.show x0) (List.cons " " (List.cons (Kind.Term.show x1) (List.cons " " (List.cons (Kind.Term.show x2) (List.cons " " (List.cons (Kind.Term.show x3) (List.cons ")" (List.nil)))))))))))))
-(Kind.Term.show.go (Kind.Term.fn5 ctid orig x0 x1 x2 x3 x4)) = (Kind.Printer.text (List.cons "(" (List.cons (NameOf ctid) (List.cons " " (List.cons (Kind.Term.show x0) (List.cons " " (List.cons (Kind.Term.show x1) (List.cons " " (List.cons (Kind.Term.show x2) (List.cons " " (List.cons (Kind.Term.show x3) (List.cons " " (List.cons (Kind.Term.show x4) (List.cons ")" (List.nil)))))))))))))))
-(Kind.Term.show.go (Kind.Term.fn6 ctid orig x0 x1 x2 x3 x4 x5)) = (Kind.Printer.text (List.cons "(" (List.cons (NameOf ctid) (List.cons " " (List.cons (Kind.Term.show x0) (List.cons " " (List.cons (Kind.Term.show x1) (List.cons " " (List.cons (Kind.Term.show x2) (List.cons " " (List.cons (Kind.Term.show x3) (List.cons " " (List.cons (Kind.Term.show x4) (List.cons " " (List.cons (Kind.Term.show x5) (List.cons ")" (List.nil)))))))))))))))))
-(Kind.Term.show.go (Kind.Term.fn7 ctid orig args)) = (Kind.Printer.text (List.cons "(" (List.cons (NameOf ctid) (List.cons " " (List.cons (Kind.Term.show args) (List.cons ")" (List.nil)))))))
-(Kind.Term.show.go (Kind.Term.fn8 ctid orig args)) = (Kind.Printer.text (List.cons "(" (List.cons (NameOf ctid) (List.cons " " (List.cons (Kind.Term.show args) (List.cons ")" (List.nil)))))))
-(Kind.Term.show.go (Kind.Term.args7 x0 x1 x2 x3 x4 x5 x6)) = (Kind.Printer.text (List.cons (Kind.Term.show x0) (List.cons " " (List.cons (Kind.Term.show x1) (List.cons " " (List.cons (Kind.Term.show x2) (List.cons " " (List.cons (Kind.Term.show x3) (List.cons " " (List.cons (Kind.Term.show x4) (List.cons " " (List.cons (Kind.Term.show x5) (List.cons " " (List.cons (Kind.Term.show x6) (List.nil)))))))))))))))
-(Kind.Term.show.go (Kind.Term.args8 x0 x1 x2 x3 x4 x5 x6 x7)) = (Kind.Printer.text (List.cons (Kind.Term.show x0) (List.cons " " (List.cons (Kind.Term.show x1) (List.cons " " (List.cons (Kind.Term.show x2) (List.cons " " (List.cons (Kind.Term.show x3) (List.cons " " (List.cons (Kind.Term.show x4) (List.cons " " (List.cons (Kind.Term.show x5) (List.cons " " (List.cons (Kind.Term.show x6) (List.cons " " (List.cons (Kind.Term.show x7) (List.nil)))))))))))))))))
-(Kind.Term.show.go (Kind.Term.hlp orig)) = "?"
-(Kind.Term.show.go (Kind.Term.u60 orig)) = "U60"
-(Kind.Term.show.go (Kind.Term.num orig numb)) = (Show.to_string (U60.show numb))
-(Kind.Term.show.go (Kind.Term.op2 orig operator left right)) = (Kind.Printer.text (List.cons "(" (List.cons (Kind.Operator.show operator) (List.cons " " (List.cons (Kind.Term.show left) (List.cons " " (List.cons (Kind.Term.show right) (List.cons ")" (List.nil)))))))))
-
-// Kind.Term.show.sugar.list.go (term: (Kind.Term)) : (Maybe (List (String)))
-(Kind.Term.show.sugar.list.go (Kind.Term.ct0 (List.nil.) orig)) = (Maybe.some (List.nil))
-(Kind.Term.show.sugar.list.go (Kind.Term.ct2 (List.cons.) orig x0 x1)) = (Maybe.bind (Kind.Term.show.sugar.list.go x1) @tail (Maybe.pure (List.cons (Kind.Term.show x0) tail)))
-(Kind.Term.show.sugar.list.go other) = (Maybe.none)
-
-// Kind.Term.show.sugar.list (term: (Kind.Term)) : (Maybe (String))
-(Kind.Term.show.sugar.list term) = (Maybe.bind (Kind.Term.show.sugar.list.go term) @res (Maybe.pure (Kind.Printer.text (List.cons "[" (List.cons (String.join " " res) (List.cons "]" (List.nil)))))))
-
-// Maybe.pure -(a: Type) (x: a) : (Maybe a)
-(Maybe.pure x) = (Maybe.some x)
-
-// String.join (sep: (String)) (list: (List (String))) : (String)
-(String.join sep list) = (String.intercalate sep list)
-
-// String.intercalate (sep: (String)) (xs: (List (String))) : (String)
-(String.intercalate sep xs) = (String.flatten (List.intersperse sep xs))
-
-// String.flatten (xs: (List (String))) : (String)
-(String.flatten (List.nil)) = ""
-(String.flatten (List.cons head tail)) = (String.concat head (String.flatten tail))
-
-// List.intersperse -(a: Type) (sep: a) (xs: (List a)) : (List a)
-(List.intersperse sep (List.nil)) = (List.nil)
-(List.intersperse sep (List.cons xh (List.nil))) = (List.pure xh)
-(List.intersperse sep (List.cons xh xt)) = (List.cons xh (List.cons sep (List.intersperse sep xt)))
-
-// List.pure -(t: Type) (x: t) : (List t)
-(List.pure x) = (List.cons x (List.nil))
-
-// Maybe.bind -(a: Type) -(b: Type) (ma: (Maybe a)) (mb: (_: a) (Maybe b)) : (Maybe b)
-(Maybe.bind (Maybe.none) mb) = (Maybe.none)
-(Maybe.bind (Maybe.some val) mb) = (mb val)
-
-// Kind.Term.show.sugar.string.go (term: (Kind.Term)) : (Maybe (String))
-(Kind.Term.show.sugar.string.go (Kind.Term.ct0 (String.nil.) orig)) = (Maybe.some "")
-(Kind.Term.show.sugar.string.go (Kind.Term.ct2 (String.cons.) orig (Kind.Term.num orig1 x0) x1)) = (Maybe.bind (Kind.Term.show.sugar.string.go x1) @tail (Maybe.pure (String.cons x0 tail)))
-(Kind.Term.show.sugar.string.go other) = (Maybe.none)
-
-// Kind.Term.show.sugar.string (term: (Kind.Term)) : (Maybe (String))
-(Kind.Term.show.sugar.string term) = (Maybe.bind (Kind.Term.show.sugar.string.go term) @res let quot = (String.cons 39 ""); (Maybe.pure (Kind.Printer.text (List.cons quot (List.cons res (List.cons quot (List.nil)))))))
-
-// Maybe.try -(a: Type) (ls: (List (Maybe a))) (alt: a) : a
-(Maybe.try (List.nil) alt) = alt
-(Maybe.try (List.cons maybe xs) alt) = (Maybe.match maybe (Maybe.try xs alt) @maybe.value maybe.value)
-
-// Kind.Term.show.sugar.sigma (term: (Kind.Term)) : (Maybe (String))
-(Kind.Term.show.sugar.sigma (Kind.Term.ct2 (Sigma.) orig typ (Kind.Term.lam orig_ name body))) = (Maybe.some (Kind.Printer.text (List.cons "([" (List.cons (Kind.Name.show name) (List.cons ": " (List.cons (Kind.Term.show typ) (List.cons "] -> " (List.cons (Kind.Term.show (body (Kind.Term.var orig_ name 0))) (List.cons ")" (List.nil))))))))))
-(Kind.Term.show.sugar.sigma term) = (Maybe.none)
-
-// Kind.Operator.show (op: (Kind.Operator)) : (String)
-(Kind.Operator.show (Kind.Operator.add)) = "+"
-(Kind.Operator.show (Kind.Operator.sub)) = "-"
-(Kind.Operator.show (Kind.Operator.mul)) = "*"
-(Kind.Operator.show (Kind.Operator.div)) = "/"
-(Kind.Operator.show (Kind.Operator.mod)) = "%"
-(Kind.Operator.show (Kind.Operator.and)) = "&"
-(Kind.Operator.show (Kind.Operator.or)) = "|"
-(Kind.Operator.show (Kind.Operator.xor)) = "^"
-(Kind.Operator.show (Kind.Operator.shl)) = "<<"
-(Kind.Operator.show (Kind.Operator.shr)) = ">>"
-(Kind.Operator.show (Kind.Operator.ltn)) = "<"
-(Kind.Operator.show (Kind.Operator.lte)) = "<="
-(Kind.Operator.show (Kind.Operator.eql)) = "=="
-(Kind.Operator.show (Kind.Operator.gte)) = ">="
-(Kind.Operator.show (Kind.Operator.gtn)) = ">"
-(Kind.Operator.show (Kind.Operator.neq)) = "!="
-
-// String.pad_right (size: (Nat)) (chr: (Char)) (str: (String)) : (String)
-(String.pad_right (Nat.zero) chr str) = str
-(String.pad_right (Nat.succ sp) chr "") = (String.cons chr (String.pad_right sp chr ""))
-(String.pad_right (Nat.succ sp) chr (String.cons x xs)) = (String.cons x (String.pad_right sp chr xs))
-
 // Pair.snd -(a: Type) -(b: Type) (pair: (Pair a b)) : b
 (Pair.snd (Pair.new fst snd)) = snd
 
-// Pair.match -(a: Type) -(b: Type) (x: (Pair a b)) -(p: (x: (Pair a b)) Type) (new: (fst: a) (snd: b) (p (Pair.new a b fst snd))) : (p x)
-(Pair.match (Pair.new fst_ snd_) new) = ((new fst_) snd_)
+// Bool.if -(a: Type) (b: (Bool)) (t: a) (f: a) : a
+(Bool.if (Bool.true) t f) = t
+(Bool.if (Bool.false) t f) = f
+
+// List.reverse -(a: Type) (xs: (List a)) : (List a)
+(List.reverse xs) = (List.reverse.go xs (List.nil))
+
+// List.reverse.go -(a: Type) (xs: (List a)) (ys: (List a)) : (List a)
+(List.reverse.go (List.nil) ys) = ys
+(List.reverse.go (List.cons x xs) ys) = (List.reverse.go xs (List.cons x ys))
 
 // Kind.API.check_functions (fnid: (List U60)) : (List (Pair U60 (List (Kind.Result (Unit)))))
 (Kind.API.check_functions (List.nil)) = (List.nil)
@@ -353,21 +366,13 @@
 (Kind.API.check_function.rules (List.nil) type) = (List.nil)
 (Kind.API.check_function.rules (List.cons rule rules) type) = let head = (Kind.Checker.run (Kind.Checker.unify (Kind.Checker.rule rule type)) (Bool.false)); let tail = (Kind.API.check_function.rules rules type); (List.cons head tail)
 
-// Kind.Checker.unify (checker: (Kind.Checker (Unit))) : (Kind.Checker (Unit))
-(Kind.Checker.unify checker) = (Kind.Checker.bind checker @_ (Kind.Checker.bind (Kind.Checker.get_equations) @equations (Kind.Checker.unify.go equations (List.nil) (Bool.false))))
+// Kind.Checker.rule (rule: (Kind.Rule)) (term: (Kind.Term)) : (Kind.Checker (Unit))
+(Kind.Checker.rule (Kind.Rule.lhs arg args) (Kind.Term.all orig name type body)) = (Kind.Checker.bind (Kind.Checker.check arg type) @_ (Kind.Checker.bind (Kind.Checker.rule args (body arg)) @_ (Kind.Checker.pure (Unit.new))))
+(Kind.Checker.rule (Kind.Rule.lhs arg args) other) = (Kind.Checker.bind (Kind.Checker.get_context) @ctx (Kind.Checker.fail (Kind.Error.too_many_arguments ctx (Kind.Term.get_origin arg @orig @term orig))))
+(Kind.Checker.rule (Kind.Rule.rhs expr) type) = (Kind.Checker.bind (Kind.Checker.set_right_hand_side (Bool.true)) @_ (Kind.Checker.bind (Kind.Checker.check expr type) @_ (Kind.Checker.pure (Unit.new))))
 
-// Kind.Checker.unify.go (equations: (List (Kind.Equation))) (unsolved: (List (Kind.Equation))) (changed: (Bool)) : (Kind.Checker (Unit))
-(Kind.Checker.unify.go (List.nil) (List.nil) changed) = (Kind.Checker.pure (Unit.new))
-(Kind.Checker.unify.go (List.nil) unsolved (Bool.true)) = (Kind.Checker.unify.go unsolved (List.nil) (Bool.false))
-(Kind.Checker.unify.go (List.nil) unsolved (Bool.false)) = (Kind.Checker.unify.go.fail unsolved)
-(Kind.Checker.unify.go (List.cons (Kind.Equation.new ctx orig left right) equations) unsolved changed) = (Kind.Checker.bind (Kind.Checker.equal (Kind.Term.eval left) (Kind.Term.eval right)) @is_equal let unify = (Bool.if is_equal @equations @unsolved (Kind.Checker.unify.go equations unsolved (Bool.true)) @equations @unsolved let eqt = (Kind.Equation.new ctx orig left right); (Kind.Checker.unify.go equations (List.cons eqt unsolved) changed)); ((unify equations) unsolved))
-
-// Kind.Checker.unify.go.fail (equations: (List (Kind.Equation))) : (Kind.Checker (Unit))
-(Kind.Checker.unify.go.fail (List.nil)) = (Kind.Checker.pure (Unit.new))
-(Kind.Checker.unify.go.fail (List.cons (Kind.Equation.new ctx orig left right) eqts)) = (Kind.Checker.bind (Kind.Checker.error (Kind.Error.type_mismatch ctx orig left right) (Unit.new)) @_ (Kind.Checker.unify.go.fail eqts))
-
-// Kind.Checker.get_equations : (Kind.Checker (List (Kind.Equation)))
-(Kind.Checker.get_equations) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked context depth rhs subst eqts errs eqts)
+// Kind.Checker.set_right_hand_side (rhs: (Bool)) : (Kind.Checker (Unit))
+(Kind.Checker.set_right_hand_side to_rhs) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked context depth to_rhs subst eqts errs (Unit.new))
 
 // Kind.Checker (a: Type) : Type
 (Kind.Checker a) = 0
@@ -379,13 +384,95 @@
 // Kind.Checker.bind -(a: Type) -(b: Type) (checker: (Kind.Checker a)) (then: (_: a) (Kind.Checker b)) : (Kind.Checker b)
 (Kind.Checker.bind checker then) = @context @depth @rhs @subst @eqts @errs (Kind.Checker.bind.result ((((((checker context) depth) rhs) subst) eqts) errs) then)
 
+// Kind.Term.get_origin -(r: Type) (term: (Kind.Term)) (got: (_: U60) (_: (Kind.Term)) r) : r
+(Kind.Term.get_origin (Kind.Term.typ orig) got) = ((got orig) (Kind.Term.typ orig))
+(Kind.Term.get_origin (Kind.Term.var orig name index) got) = ((got orig) (Kind.Term.var orig name index))
+(Kind.Term.get_origin (Kind.Term.hol orig numb) got) = ((got orig) (Kind.Term.hol orig numb))
+(Kind.Term.get_origin (Kind.Term.all orig name typ body) got) = ((got orig) (Kind.Term.all orig name typ body))
+(Kind.Term.get_origin (Kind.Term.lam orig name body) got) = ((got orig) (Kind.Term.lam orig name body))
+(Kind.Term.get_origin (Kind.Term.let orig name expr body) got) = ((got orig) (Kind.Term.let orig name expr body))
+(Kind.Term.get_origin (Kind.Term.ann orig expr typ) got) = ((got orig) (Kind.Term.ann orig expr typ))
+(Kind.Term.get_origin (Kind.Term.sub orig name indx redx expr) got) = ((got orig) (Kind.Term.sub orig name indx redx expr))
+(Kind.Term.get_origin (Kind.Term.app orig func arg) got) = ((got orig) (Kind.Term.app orig func arg))
+(Kind.Term.get_origin (Kind.Term.hlp orig) got) = ((got orig) (Kind.Term.hlp orig))
+(Kind.Term.get_origin (Kind.Term.u60 orig) got) = ((got orig) (Kind.Term.u60 orig))
+(Kind.Term.get_origin (Kind.Term.num orig num) got) = ((got orig) (Kind.Term.num orig num))
+(Kind.Term.get_origin (Kind.Term.op2 orig op left right) got) = ((got orig) (Kind.Term.op2 orig op left right))
+(Kind.Term.get_origin (Kind.Term.ct0 ctid orig) got) = ((got orig) (Kind.Term.ct0 ctid orig))
+(Kind.Term.get_origin (Kind.Term.ct1 ctid orig x0) got) = ((got orig) (Kind.Term.ct1 ctid orig x0))
+(Kind.Term.get_origin (Kind.Term.ct2 ctid orig x0 x1) got) = ((got orig) (Kind.Term.ct2 ctid orig x0 x1))
+(Kind.Term.get_origin (Kind.Term.ct3 ctid orig x0 x1 x2) got) = ((got orig) (Kind.Term.ct3 ctid orig x0 x1 x2))
+(Kind.Term.get_origin (Kind.Term.ct4 ctid orig x0 x1 x2 x3) got) = ((got orig) (Kind.Term.ct4 ctid orig x0 x1 x2 x3))
+(Kind.Term.get_origin (Kind.Term.ct5 ctid orig x0 x1 x2 x3 x4) got) = ((got orig) (Kind.Term.ct5 ctid orig x0 x1 x2 x3 x4))
+(Kind.Term.get_origin (Kind.Term.ct6 ctid orig x0 x1 x2 x3 x4 x5) got) = ((got orig) (Kind.Term.ct6 ctid orig x0 x1 x2 x3 x4 x5))
+(Kind.Term.get_origin (Kind.Term.ct7 ctid orig args) got) = ((got orig) (Kind.Term.ct7 ctid orig args))
+(Kind.Term.get_origin (Kind.Term.ct8 ctid orig args) got) = ((got orig) (Kind.Term.ct8 ctid orig args))
+(Kind.Term.get_origin (Kind.Term.fn0 fnid orig) got) = ((got orig) (Kind.Term.fn0 fnid orig))
+(Kind.Term.get_origin (Kind.Term.fn1 fnid orig x0) got) = ((got orig) (Kind.Term.fn1 fnid orig x0))
+(Kind.Term.get_origin (Kind.Term.fn2 fnid orig x0 x1) got) = ((got orig) (Kind.Term.fn2 fnid orig x0 x1))
+(Kind.Term.get_origin (Kind.Term.fn3 fnid orig x0 x1 x2) got) = ((got orig) (Kind.Term.fn3 fnid orig x0 x1 x2))
+(Kind.Term.get_origin (Kind.Term.fn4 fnid orig x0 x1 x2 x3) got) = ((got orig) (Kind.Term.fn4 fnid orig x0 x1 x2 x3))
+(Kind.Term.get_origin (Kind.Term.fn5 fnid orig x0 x1 x2 x3 x4) got) = ((got orig) (Kind.Term.fn5 fnid orig x0 x1 x2 x3 x4))
+(Kind.Term.get_origin (Kind.Term.fn6 fnid orig x0 x1 x2 x3 x4 x5) got) = ((got orig) (Kind.Term.fn6 fnid orig x0 x1 x2 x3 x4 x5))
+(Kind.Term.get_origin (Kind.Term.fn7 fnid orig args) got) = ((got orig) (Kind.Term.fn7 fnid orig args))
+(Kind.Term.get_origin (Kind.Term.fn8 fnid orig args) got) = ((got orig) (Kind.Term.fn8 fnid orig args))
+
+// Kind.Checker.check (term: (Kind.Term)) (type: (Kind.Term)) : (Kind.Checker (Unit))
+(Kind.Checker.check (Kind.Term.lam orig name body) type) = (Kind.Checker.bind (Kind.Checker.get_subst) @subst let fun = (Kind.Term.if_all type @t_orig @t_name @t_type @t_body @orig @name @body (Kind.Checker.bind (Kind.Checker.get_depth) @dep (Kind.Checker.bind (Kind.Checker.extended (Kind.Checker.check (body (Kind.Term.var orig name dep)) (t_body (Kind.Term.var t_orig t_name dep))) name t_type (List.nil)) @chk (Kind.Checker.pure (Unit.new)))) @orig @name @body (Kind.Checker.bind (Kind.Checker.get_context) @ctx (Kind.Checker.fail (Kind.Error.cant_infer_lambda ctx orig)))); (((fun orig) name) body))
+(Kind.Checker.check (Kind.Term.let orig name expr body) type) = (Kind.Checker.bind (Kind.Checker.get_depth) @dep (Kind.Checker.bind (Kind.Checker.infer expr) @expr_typ (Kind.Checker.bind (Kind.Checker.extended (Kind.Checker.check (body (Kind.Term.var orig name dep)) type) name expr_typ (List.cons (Kind.Term.eval expr) (List.nil))) @body_chk (Kind.Checker.pure (Unit.new)))))
+(Kind.Checker.check (Kind.Term.hlp orig) type) = (Kind.Checker.bind (Kind.Checker.get_context) @ctx (Kind.Checker.bind (Kind.Checker.error (Kind.Error.inspection ctx orig type) (Unit.new)) @_ (Kind.Checker.pure (Unit.new))))
+(Kind.Checker.check (Kind.Term.var orig name idx) type) = (Kind.Checker.bind (Kind.Checker.get_right_hand_side) @rhs (Bool.if rhs (Kind.Checker.compare rhs (Kind.Term.var orig name idx) type) (Kind.Checker.extend name type (List.nil))))
+(Kind.Checker.check (Kind.Term.hol orig numb) type) = (Kind.Checker.pure (Unit.new))
+(Kind.Checker.check term type) = (Kind.Checker.bind (Kind.Checker.get_right_hand_side) @rhs (Kind.Checker.compare rhs term type))
+
+// Kind.Checker.compare (rhs: (Bool)) (term: (Kind.Term)) (type: (Kind.Term)) : (Kind.Checker (Unit))
+(Kind.Checker.compare rhs term type) = (Kind.Term.get_origin term @orig @term (Kind.Checker.bind (Kind.Checker.infer term) @term_typ let fun = (Bool.if rhs @term_typ @type (Kind.Checker.new_equation orig type term_typ) @term_typ @type (Kind.Checker.bind (Kind.Checker.equal (Kind.Term.eval term_typ) (Kind.Term.eval type)) @is_equal (Bool.if is_equal (Kind.Checker.pure (Unit.new)) (Kind.Checker.bind (Kind.Checker.get_context) @ctx (Kind.Checker.fail (Kind.Error.impossible_case ctx orig type term_typ)))))); ((fun term_typ) type)))
+
+// Kind.Checker.new_equation (orig: U60) (left: (Kind.Term)) (right: (Kind.Term)) : (Kind.Checker (Unit))
+(Kind.Checker.new_equation orig left right) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked context depth rhs subst (List.append eqts (Kind.Equation.new context orig left right)) errs (Unit.new))
+
+// List.append -(a: Type) (xs: (List a)) (x: a) : (List a)
+(List.append (List.nil) x) = (List.pure x)
+(List.append (List.cons xs.h xs.t) x) = (List.cons xs.h (List.append xs.t x))
+
+// Kind.Checker.error -(t: Type) (err: (Kind.Error)) (ret: t) : (Kind.Checker t)
+(Kind.Checker.error err ret) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked context depth rhs subst eqts (List.cons err errs) ret)
+
+// Kind.Checker.get_context : (Kind.Checker (Kind.Context))
+(Kind.Checker.get_context) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked context depth rhs subst eqts errs context)
+
+// Kind.Checker.extended -(a: Type) (checker: (Kind.Checker a)) (name: U60) (type: (Kind.Term)) (vals: (List (Kind.Term))) : (Kind.Checker a)
+(Kind.Checker.extended checker name type vals) = (Kind.Checker.bind (Kind.Checker.extend name type vals) @_ (Kind.Checker.bind checker @got (Kind.Checker.bind (Kind.Checker.shrink) @_ (Kind.Checker.pure got))))
+
+// Kind.Checker.pure -(t: Type) (a: t) : (Kind.Checker t)
+(Kind.Checker.pure res) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked context depth rhs subst eqts errs res)
+
+// Kind.Checker.shrink : (Kind.Checker (Unit))
+(Kind.Checker.shrink) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked (Kind.Context.shrink context) (- depth 1) rhs subst eqts errs (Unit.new))
+
+// Kind.Context.shrink (ctx: (Kind.Context)) : (Kind.Context)
+(Kind.Context.shrink (Kind.Context.empty)) = (Kind.Context.empty)
+(Kind.Context.shrink (Kind.Context.entry name type vals (Kind.Context.empty))) = (Kind.Context.empty)
+(Kind.Context.shrink (Kind.Context.entry name type vals rest)) = (Kind.Context.entry name type vals (Kind.Context.shrink rest))
+
+// Kind.Checker.extend (name: U60) (type: (Kind.Term)) (vals: (List (Kind.Term))) : (Kind.Checker (Unit))
+(Kind.Checker.extend name type vals) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked (Kind.Context.extend context name type vals) (+ depth 1) rhs subst eqts errs (Unit.new))
+
+// Kind.Context.extend (prev: (Kind.Context)) (name: U60) (term: (Kind.Term)) (ls: (List (Kind.Term))) : (Kind.Context)
+(Kind.Context.extend (Kind.Context.empty) name type values) = (Kind.Context.entry name type values (Kind.Context.empty))
+(Kind.Context.extend (Kind.Context.entry n t v rest) name type values) = (Kind.Context.entry n t v (Kind.Context.extend rest name type values))
+
+// Kind.Checker.fail -(t: Type) (err: (Kind.Error)) : (Kind.Checker t)
+(Kind.Checker.fail err) = @context @depth @rhs @subst @eqts @errs (Kind.Result.errored context subst (List.cons err errs))
+
 // Kind.Checker.equal (left: (Kind.Term)) (right: (Kind.Term)) : (Kind.Checker (Bool))
 (Kind.Checker.equal (Kind.Term.typ orig) (Kind.Term.typ orig1)) = (Kind.Checker.pure (Bool.true))
 (Kind.Checker.equal (Kind.Term.all a.orig a.name a.type a.body) (Kind.Term.all b.orig b.name b.type b.body)) = (Kind.Checker.bind (Kind.Checker.get_depth) @dep (Kind.Checker.bind (Kind.Checker.equal a.type b.type) @type (Kind.Checker.bind (Kind.Checker.extended (Kind.Checker.equal (a.body (Kind.Term.var a.orig a.name dep)) (b.body (Kind.Term.var b.orig b.name dep))) (Null) (Null) (List.nil)) @body (Kind.Checker.pure (Bool.and type body)))))
 (Kind.Checker.equal (Kind.Term.lam a.orig a.name a.body) (Kind.Term.lam b.orig b.name b.body)) = (Kind.Checker.bind (Kind.Checker.get_depth) @dep (Kind.Checker.bind (Kind.Checker.extended (Kind.Checker.equal (a.body (Kind.Term.var a.orig a.name dep)) (b.body (Kind.Term.var b.orig b.name dep))) (Null) (Null) (List.nil)) @body (Kind.Checker.pure body)))
 (Kind.Checker.equal (Kind.Term.app a.orig a.func a.argm) (Kind.Term.app b.orig b.func b.argm)) = (Kind.Checker.bind (Kind.Checker.equal a.func b.func) @func (Kind.Checker.bind (Kind.Checker.equal a.argm b.argm) @argm (Kind.Checker.pure (Bool.and func argm))))
 (Kind.Checker.equal (Kind.Term.let a.orig a.name a.expr a.body) (Kind.Term.let b.orig b.name b.expr b.body)) = (Kind.Checker.bind (Kind.Checker.get_depth) @dep (Kind.Checker.bind (Kind.Checker.equal a.expr b.expr) @expr (Kind.Checker.bind (Kind.Checker.extended (Kind.Checker.equal (a.body (Kind.Term.var a.orig a.name dep)) (b.body (Kind.Term.var b.orig b.name dep))) (Null) (Null) (List.nil)) @body (Kind.Checker.pure (Bool.and expr body)))))
-(Kind.Checker.equal (Kind.Term.ann a.orig a.expr a.type) (Kind.Term.ann b.orig b.expr b.type)) = (Kind.Checker.bind (Kind.Checker.equal a.expr b.expr) @func (Kind.Checker.bind (Kind.Checker.equal a.type b.type) @arg (Kind.Checker.pure (Bool.and func arg))))
+(Kind.Checker.equal (Kind.Term.ann a.orig a.expr a.type) (Kind.Term.ann b.orig b.expr b.type)) = (Kind.Checker.bind (Kind.Checker.equal a.expr b.expr) @func (Kind.Checker.bind (Kind.Checker.equal a.type b.type) @type (Kind.Checker.pure (Bool.and func type))))
+(Kind.Checker.equal (Kind.Term.sub a.orig a.name a.indx a.redx a.expr) (Kind.Term.sub b.orig b.name b.indx b.redx b.expr)) = (Kind.Checker.bind (Kind.Checker.equal a.expr b.expr) @func (Kind.Checker.pure func))
 (Kind.Checker.equal (Kind.Term.u60 a.orig) (Kind.Term.u60 b.orig)) = (Kind.Checker.pure (Bool.true))
 (Kind.Checker.equal (Kind.Term.num a.orig a.num) (Kind.Term.num b.orig b.num)) = (Kind.Checker.pure (U60.equal a.num b.num))
 (Kind.Checker.equal (Kind.Term.op2 a.orig a.op a.val0 a.val1) (Kind.Term.op2 b.orig b.op b.val0 b.val1)) = let op = (Kind.Operator.equal a.op b.op); (Kind.Checker.bind (Kind.Checker.equal a.val0 b.val0) @val0 (Kind.Checker.bind (Kind.Checker.equal a.val1 b.val1) @val1 (Kind.Checker.pure (Bool.and op (Bool.and val0 val1)))))
@@ -432,6 +519,14 @@
 (Kind.Checker.equal.hol.val (Maybe.none) orig numb b) = (Kind.Checker.bind (Kind.Checker.fill numb b) @_ (Kind.Checker.pure (Bool.true)))
 (Kind.Checker.equal.hol.val (Maybe.some val) orig numb b) = (Kind.Checker.equal val b)
 
+// Kind.Checker.find -(r: Type) (index: U60) (alt: r) (fun: (_: U60) (_: (Kind.Term)) (_: (List (Kind.Term))) r) : (Kind.Checker r)
+(Kind.Checker.find index alt fun) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked context depth rhs subst eqts errs (Kind.Context.find context index alt fun))
+
+// Kind.Context.find -(res: Type) (ctx: (Kind.Context)) (name: U60) (alt: res) (fun: (_: U60) (_: (Kind.Term)) (_: (List (Kind.Term))) res) : res
+(Kind.Context.find (Kind.Context.entry name type vals rest) 0 alt fun) = (((fun name) type) vals)
+(Kind.Context.find (Kind.Context.entry name type vals rest) n alt fun) = (Kind.Context.find rest (- n 1) alt fun)
+(Kind.Context.find (Kind.Context.empty) n alt fun) = alt
+
 // U60.equal (a: U60) (b: U60) : (Bool)
 (U60.equal a b) = (U60.to_bool (== a b))
 
@@ -464,68 +559,6 @@
 // Kind.Checker.get_subst : (Kind.Checker (Kind.Subst))
 (Kind.Checker.get_subst) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked context depth rhs subst eqts errs subst)
 
-// Bool.and (a: (Bool)) (b: (Bool)) : (Bool)
-(Bool.and (Bool.true) b) = b
-(Bool.and (Bool.false) b) = (Bool.false)
-
-// Kind.Checker.extended -(a: Type) (checker: (Kind.Checker a)) (name: U60) (type: (Kind.Term)) (vals: (List (Kind.Term))) : (Kind.Checker a)
-(Kind.Checker.extended checker name type vals) = (Kind.Checker.bind (Kind.Checker.extend name type vals) @_ (Kind.Checker.bind checker @got (Kind.Checker.bind (Kind.Checker.shrink) @_ (Kind.Checker.pure got))))
-
-// Kind.Checker.shrink : (Kind.Checker (Unit))
-(Kind.Checker.shrink) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked (Kind.Context.shrink context) (- depth 1) rhs subst eqts errs (Unit.new))
-
-// Kind.Context.shrink (ctx: (Kind.Context)) : (Kind.Context)
-(Kind.Context.shrink (Kind.Context.empty)) = (Kind.Context.empty)
-(Kind.Context.shrink (Kind.Context.entry name type vals (Kind.Context.empty))) = (Kind.Context.empty)
-(Kind.Context.shrink (Kind.Context.entry name type vals rest)) = (Kind.Context.entry name type vals (Kind.Context.shrink rest))
-
-// Kind.Checker.pure -(t: Type) (a: t) : (Kind.Checker t)
-(Kind.Checker.pure res) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked context depth rhs subst eqts errs res)
-
-// Kind.Checker.extend (name: U60) (type: (Kind.Term)) (vals: (List (Kind.Term))) : (Kind.Checker (Unit))
-(Kind.Checker.extend name type vals) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked (Kind.Context.extend context name type vals) (+ depth 1) rhs subst eqts errs (Unit.new))
-
-// Kind.Context.extend (prev: (Kind.Context)) (name: U60) (term: (Kind.Term)) (ls: (List (Kind.Term))) : (Kind.Context)
-(Kind.Context.extend (Kind.Context.empty) name type values) = (Kind.Context.entry name type values (Kind.Context.empty))
-(Kind.Context.extend (Kind.Context.entry n t v rest) name type values) = (Kind.Context.entry n t v (Kind.Context.extend rest name type values))
-
-// Kind.Checker.look (index: U60) : (Kind.Checker (Maybe (Kind.Term)))
-(Kind.Checker.look index) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked context depth rhs subst eqts errs (Kind.Subst.look subst index))
-
-// Kind.Checker.get_depth : (Kind.Checker U60)
-(Kind.Checker.get_depth) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked context depth rhs subst eqts errs depth)
-
-// Kind.Checker.fill (index: U60) (val: (Kind.Term)) : (Kind.Checker (Unit))
-(Kind.Checker.fill index val) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked context depth rhs (Kind.Subst.fill subst index val) eqts errs (Unit.new))
-
-// Kind.Subst.fill (subst: (Kind.Subst)) (depth: U60) (term: (Kind.Term)) : (Kind.Subst)
-(Kind.Subst.fill (Kind.Subst.end) 0 term) = (Kind.Subst.sub term (Kind.Subst.end))
-(Kind.Subst.fill (Kind.Subst.unfilled rest) 0 term) = (Kind.Subst.sub term rest)
-(Kind.Subst.fill (Kind.Subst.sub lost rest) 0 term) = (Kind.Subst.sub term rest)
-(Kind.Subst.fill (Kind.Subst.end) n term) = (Kind.Subst.unfilled (Kind.Subst.fill (Kind.Subst.end) (- n 1) term))
-(Kind.Subst.fill (Kind.Subst.unfilled rest) n term) = (Kind.Subst.unfilled (Kind.Subst.fill rest (- n 1) term))
-(Kind.Subst.fill (Kind.Subst.sub keep rest) n term) = (Kind.Subst.sub keep (Kind.Subst.fill rest (- n 1) term))
-
-// Kind.Checker.add_value (idx: U60) (val: (Kind.Term)) : (Kind.Checker (Unit))
-(Kind.Checker.add_value idx val) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked (Kind.Context.add_value context idx val) depth rhs subst eqts errs (Unit.new))
-
-// Kind.Context.add_value (prev: (Kind.Context)) (name: U60) (term: (Kind.Term)) : (Kind.Context)
-(Kind.Context.add_value (Kind.Context.entry name type vals rest) 0 val) = (Kind.Context.entry name type (List.cons val vals) rest)
-(Kind.Context.add_value (Kind.Context.entry name type vals rest) n val) = (Kind.Context.entry name type vals (Kind.Context.add_value rest (- n 1) val))
-(Kind.Context.add_value (Kind.Context.empty) n val) = (Kind.Context.empty)
-
-// Bool.or (a: (Bool)) (b: (Bool)) : (Bool)
-(Bool.or (Bool.true) b) = (Bool.true)
-(Bool.or (Bool.false) b) = b
-
-// Kind.Checker.find -(r: Type) (index: U60) (alt: r) (fun: (_: U60) (_: (Kind.Term)) (_: (List (Kind.Term))) r) : (Kind.Checker r)
-(Kind.Checker.find index alt fun) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked context depth rhs subst eqts errs (Kind.Context.find context index alt fun))
-
-// Kind.Context.find -(res: Type) (ctx: (Kind.Context)) (name: U60) (alt: res) (fun: (_: U60) (_: (Kind.Term)) (_: (List (Kind.Term))) res) : res
-(Kind.Context.find (Kind.Context.entry name type vals rest) 0 alt fun) = (((fun name) type) vals)
-(Kind.Context.find (Kind.Context.entry name type vals rest) n alt fun) = (Kind.Context.find rest (- n 1) alt fun)
-(Kind.Context.find (Kind.Context.empty) n alt fun) = alt
-
 // Kind.Term.fillable (term: (Kind.Term)) (sub: (Kind.Subst)) : (Bool)
 (Kind.Term.fillable term (Kind.Subst.end)) = (Bool.false)
 (Kind.Term.fillable (Kind.Term.typ orig) sub) = (Bool.false)
@@ -538,6 +571,7 @@
 (Kind.Term.fillable (Kind.Term.app orig expr typ) sub) = (Bool.or (Kind.Term.fillable expr sub) (Kind.Term.fillable typ sub))
 (Kind.Term.fillable (Kind.Term.let orig name expr body) sub) = (Bool.or (Kind.Term.fillable expr sub) (Kind.Term.fillable (body (Kind.Term.hlp 0)) sub))
 (Kind.Term.fillable (Kind.Term.ann orig expr typ) sub) = (Bool.or (Kind.Term.fillable expr sub) (Kind.Term.fillable typ sub))
+(Kind.Term.fillable (Kind.Term.sub orig name indx redx expr) sub) = (Kind.Term.fillable expr sub)
 (Kind.Term.fillable (Kind.Term.op2 orig op left right) sub) = (Bool.or (Kind.Term.fillable left sub) (Kind.Term.fillable right sub))
 (Kind.Term.fillable (Kind.Term.hol orig numb) sub) = (Maybe.is_some (Kind.Subst.look sub numb))
 (Kind.Term.fillable (Kind.Term.ct0 ctid orig) sub) = (Bool.false)
@@ -561,10 +595,119 @@
 (Kind.Term.fillable (Kind.Term.args7 x0 x1 x2 x3 x4 x5 x6) sub) = (Bool.or (Kind.Term.fillable x0 sub) (Bool.or (Kind.Term.fillable x1 sub) (Bool.or (Kind.Term.fillable x2 sub) (Bool.or (Kind.Term.fillable x3 sub) (Bool.or (Kind.Term.fillable x4 sub) (Bool.or (Kind.Term.fillable x5 sub) (Kind.Term.fillable x6 sub)))))))
 (Kind.Term.fillable (Kind.Term.args8 x0 x1 x2 x3 x4 x5 x6 x7) sub) = (Bool.or (Kind.Term.fillable x0 sub) (Bool.or (Kind.Term.fillable x1 sub) (Bool.or (Kind.Term.fillable x2 sub) (Bool.or (Kind.Term.fillable x3 sub) (Bool.or (Kind.Term.fillable x4 sub) (Bool.or (Kind.Term.fillable x5 sub) (Bool.or (Kind.Term.fillable x6 sub) (Kind.Term.fillable x7 sub))))))))
 
+// Bool.or (a: (Bool)) (b: (Bool)) : (Bool)
+(Bool.or (Bool.true) b) = (Bool.true)
+(Bool.or (Bool.false) b) = b
+
 // Maybe.is_some -(a: Type) (m: (Maybe a)) : (Bool)
 (Maybe.is_some (Maybe.none)) = (Bool.false)
 (Maybe.is_some (Maybe.some v)) = (Bool.true)
 
+// Kind.Checker.get_depth : (Kind.Checker U60)
+(Kind.Checker.get_depth) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked context depth rhs subst eqts errs depth)
+
+// Kind.Checker.add_value (idx: U60) (val: (Kind.Term)) : (Kind.Checker (Unit))
+(Kind.Checker.add_value idx val) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked (Kind.Context.add_value context idx val) depth rhs subst eqts errs (Unit.new))
+
+// Kind.Context.add_value (prev: (Kind.Context)) (name: U60) (term: (Kind.Term)) : (Kind.Context)
+(Kind.Context.add_value (Kind.Context.entry name type vals rest) 0 val) = (Kind.Context.entry name type (List.cons val vals) rest)
+(Kind.Context.add_value (Kind.Context.entry name type vals rest) n val) = (Kind.Context.entry name type vals (Kind.Context.add_value rest (- n 1) val))
+(Kind.Context.add_value (Kind.Context.empty) n val) = (Kind.Context.empty)
+
+// Kind.Checker.look (index: U60) : (Kind.Checker (Maybe (Kind.Term)))
+(Kind.Checker.look index) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked context depth rhs subst eqts errs (Kind.Subst.look subst index))
+
+// Bool.and (a: (Bool)) (b: (Bool)) : (Bool)
+(Bool.and (Bool.true) b) = b
+(Bool.and (Bool.false) b) = (Bool.false)
+
+// Kind.Checker.fill (index: U60) (val: (Kind.Term)) : (Kind.Checker (Unit))
+(Kind.Checker.fill index val) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked context depth rhs (Kind.Subst.fill subst index val) eqts errs (Unit.new))
+
+// Kind.Subst.fill (subst: (Kind.Subst)) (depth: U60) (term: (Kind.Term)) : (Kind.Subst)
+(Kind.Subst.fill (Kind.Subst.end) 0 term) = (Kind.Subst.sub term (Kind.Subst.end))
+(Kind.Subst.fill (Kind.Subst.unfilled rest) 0 term) = (Kind.Subst.sub term rest)
+(Kind.Subst.fill (Kind.Subst.sub lost rest) 0 term) = (Kind.Subst.sub term rest)
+(Kind.Subst.fill (Kind.Subst.end) n term) = (Kind.Subst.unfilled (Kind.Subst.fill (Kind.Subst.end) (- n 1) term))
+(Kind.Subst.fill (Kind.Subst.unfilled rest) n term) = (Kind.Subst.unfilled (Kind.Subst.fill rest (- n 1) term))
+(Kind.Subst.fill (Kind.Subst.sub keep rest) n term) = (Kind.Subst.sub keep (Kind.Subst.fill rest (- n 1) term))
+
+// Kind.Checker.infer_args (args: (Kind.Term)) : (_: U60) (_: U60) (Kind.Term)
+(Kind.Checker.infer_args (Kind.Term.args7 x0 x1 x2 x3 x4 x5 x6)) = @ctid @orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.fn0 ctid orig) x0) x1) x2) x3) x4) x5) x6)
+(Kind.Checker.infer_args (Kind.Term.args8 x0 x1 x2 x3 x4 x5 x6 x7)) = @ctid @orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.ct0 ctid orig) x0) x1) x2) x3) x4) x5) x6) x7)
+
+// Kind.Checker.infer (term: (Kind.Term)) : (Kind.Checker (Kind.Term))
+(Kind.Checker.infer (Kind.Term.var orig name index)) = (Kind.Checker.bind (Kind.Checker.find index (Maybe.none) @n @t @v (Maybe.some t)) @got_type (Maybe.match got_type (Kind.Checker.bind (Kind.Checker.get_context) @ctx (Kind.Checker.fail (Kind.Error.unbound_variable ctx orig))) @got_type.value (Kind.Checker.pure got_type.value)))
+(Kind.Checker.infer (Kind.Term.hol orig numb)) = (Kind.Checker.bind (Kind.Checker.get_context) @ctx (Kind.Checker.fail (Kind.Error.cant_infer_hole ctx orig)))
+(Kind.Checker.infer (Kind.Term.typ orig)) = (Kind.Checker.pure (Kind.Term.typ orig))
+(Kind.Checker.infer (Kind.Term.all orig name type body)) = (Kind.Checker.bind (Kind.Checker.get_depth) @depth (Kind.Checker.bind (Kind.Checker.check type (Kind.Term.typ orig)) @_ (Kind.Checker.bind (Kind.Checker.extended (Kind.Checker.check (body (Kind.Term.var orig name depth)) (Kind.Term.typ orig)) name (Kind.Term.eval type) (List.nil)) @_ (Kind.Checker.pure (Kind.Term.typ orig)))))
+(Kind.Checker.infer (Kind.Term.lam orig name body)) = (Kind.Checker.bind (Kind.Checker.get_context) @ctx (Kind.Checker.fail (Kind.Error.cant_infer_lambda ctx orig)))
+(Kind.Checker.infer (Kind.Term.app orig func argm)) = (Kind.Checker.bind (Kind.Checker.get_subst) @subst (Kind.Checker.bind (Kind.Checker.infer func) @func_typ (Kind.Term.if_all func_typ @func_orig @func_name @func_type @func_body (Kind.Checker.bind (Kind.Checker.check argm func_type) @_ (Kind.Checker.pure (func_body (Kind.Term.eval argm)))) (Kind.Checker.bind (Kind.Checker.get_context) @ctx (Kind.Checker.fail (Kind.Error.invalid_call ctx orig))))))
+(Kind.Checker.infer (Kind.Term.let orig name expr body)) = (Kind.Checker.bind (Kind.Checker.get_depth) @dep (Kind.Checker.bind (Kind.Checker.infer expr) @expr_typ (Kind.Checker.bind (Kind.Checker.extended (Kind.Checker.infer (body (Kind.Term.var orig name dep))) name expr_typ (List.cons (Kind.Term.eval expr) (List.nil))) @body_typ (Kind.Checker.pure body_typ))))
+(Kind.Checker.infer (Kind.Term.ann orig expr type)) = let type = (Kind.Term.eval type); (Kind.Checker.bind (Kind.Checker.check expr type) @_ (Kind.Checker.pure type))
+(Kind.Checker.infer (Kind.Term.sub orig name indx redx expr)) = (Kind.Checker.bind (Kind.Checker.get_depth) @dep (Kind.Checker.bind (Kind.Checker.find indx (Maybe.none) @n @t @v (Maybe.some (Pair.new t v))) @got (Maybe.match got (Kind.Checker.bind (Kind.Checker.get_context) @ctx (Kind.Checker.fail (Kind.Error.unbound_variable ctx orig))) @got.value (Pair.match got.value @got.value.fst @got.value.snd (Maybe.match (List.at.u60 got.value.snd redx) (Kind.Checker.bind (Kind.Checker.get_context) @ctx (Kind.Checker.fail (Kind.Error.unbound_variable ctx orig))) @reduction.value (Kind.Checker.bind (Kind.Checker.infer expr) @expr_typ (Kind.Checker.pure (Kind.Term.eval (Kind.Term.replace expr_typ indx reduction.value)))))))))
+(Kind.Checker.infer (Kind.Term.ct0 ctid orig)) = (Kind.Checker.pure (Kind.Term.eval (TypeOf ctid)))
+(Kind.Checker.infer (Kind.Term.ct1 ctid orig x0)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.ct0 ctid orig) x0))
+(Kind.Checker.infer (Kind.Term.ct2 ctid orig x0 x1)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.ct0 ctid orig) x0) x1))
+(Kind.Checker.infer (Kind.Term.ct3 ctid orig x0 x1 x2)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.ct0 ctid orig) x0) x1) x2))
+(Kind.Checker.infer (Kind.Term.ct4 ctid orig x0 x1 x2 x3)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.ct0 ctid orig) x0) x1) x2) x3))
+(Kind.Checker.infer (Kind.Term.ct5 ctid orig x0 x1 x2 x3 x4)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.ct0 ctid orig) x0) x1) x2) x3) x4))
+(Kind.Checker.infer (Kind.Term.ct6 ctid orig x0 x1 x2 x3 x4 x5)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.ct0 ctid orig) x0) x1) x2) x3) x4) x5))
+(Kind.Checker.infer (Kind.Term.ct7 ctid orig args)) = let expr = (Kind.Checker.infer_args args); (Kind.Checker.infer ((expr ctid) orig))
+(Kind.Checker.infer (Kind.Term.ct8 ctid orig args)) = let expr = (Kind.Checker.infer_args args); (Kind.Checker.infer ((expr ctid) orig))
+(Kind.Checker.infer (Kind.Term.fn0 ctid orig)) = (Kind.Checker.pure (Kind.Term.eval (TypeOf ctid)))
+(Kind.Checker.infer (Kind.Term.fn1 ctid orig x0)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.fn0 ctid orig) x0))
+(Kind.Checker.infer (Kind.Term.fn2 ctid orig x0 x1)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.fn0 ctid orig) x0) x1))
+(Kind.Checker.infer (Kind.Term.fn3 ctid orig x0 x1 x2)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.fn0 ctid orig) x0) x1) x2))
+(Kind.Checker.infer (Kind.Term.fn4 ctid orig x0 x1 x2 x3)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.fn0 ctid orig) x0) x1) x2) x3))
+(Kind.Checker.infer (Kind.Term.fn5 ctid orig x0 x1 x2 x3 x4)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.fn0 ctid orig) x0) x1) x2) x3) x4))
+(Kind.Checker.infer (Kind.Term.fn6 ctid orig x0 x1 x2 x3 x4 x5)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.fn0 ctid orig) x0) x1) x2) x3) x4) x5))
+(Kind.Checker.infer (Kind.Term.fn7 ctid orig args)) = let expr = (Kind.Checker.infer_args args); (Kind.Checker.infer ((expr ctid) orig))
+(Kind.Checker.infer (Kind.Term.fn8 ctid orig args)) = let expr = (Kind.Checker.infer_args args); (Kind.Checker.infer ((expr ctid) orig))
+(Kind.Checker.infer (Kind.Term.hlp orig)) = (Kind.Checker.bind (Kind.Checker.get_context) @ctx (Kind.Checker.fail (Kind.Error.inspection ctx orig (Kind.Term.hlp 0))))
+(Kind.Checker.infer (Kind.Term.u60 orig)) = (Kind.Checker.pure (Kind.Term.typ 0))
+(Kind.Checker.infer (Kind.Term.num orig numb)) = (Kind.Checker.pure (Kind.Term.u60 0))
+(Kind.Checker.infer (Kind.Term.op2 orig oper left right)) = (Kind.Checker.bind (Kind.Checker.check left (Kind.Term.u60 0)) @_ (Kind.Checker.bind (Kind.Checker.check right (Kind.Term.u60 0)) @_ (Kind.Checker.pure (Kind.Term.u60 0))))
+
+// Kind.Term.replace (term: (Kind.Term)) (index: U60) (value: (Kind.Term)) : (Kind.Term)
+(Kind.Term.replace (Kind.Term.typ orig) idx val) = (Kind.Term.typ orig)
+(Kind.Term.replace (Kind.Term.var orig name index) idx val) = (Bool.if (U60.equal idx index) val (Kind.Term.var orig name index))
+(Kind.Term.replace (Kind.Term.all orig name typ body) idx val) = (Kind.Term.all orig name (Kind.Term.replace typ idx val) @x (Kind.Term.replace (body x) idx val))
+(Kind.Term.replace (Kind.Term.lam orig name body) idx val) = (Kind.Term.lam orig name @x (Kind.Term.replace (body x) idx val))
+(Kind.Term.replace (Kind.Term.let orig name expr body) idx val) = (Kind.Term.let orig name (Kind.Term.replace expr idx val) @x (Kind.Term.replace (body x) idx val))
+(Kind.Term.replace (Kind.Term.ann orig expr typ) idx val) = (Kind.Term.ann orig (Kind.Term.replace expr idx val) (Kind.Term.replace typ idx val))
+(Kind.Term.replace (Kind.Term.sub orig name indx redx expr) idx val) = (Kind.Term.sub orig name indx redx (Kind.Term.replace expr idx val))
+(Kind.Term.replace (Kind.Term.app orig expr typ) idx val) = (Kind.Term.app orig (Kind.Term.replace expr idx val) (Kind.Term.replace typ idx val))
+(Kind.Term.replace (Kind.Term.hlp orig) idx val) = (Kind.Term.hlp orig)
+(Kind.Term.replace (Kind.Term.u60 orig) idx val) = (Kind.Term.u60 orig)
+(Kind.Term.replace (Kind.Term.num orig num) idx val) = (Kind.Term.num orig num)
+(Kind.Term.replace (Kind.Term.op2 orig op left right) idx val) = (Kind.Term.op2 orig op (Kind.Term.replace left idx val) (Kind.Term.replace right idx val))
+(Kind.Term.replace (Kind.Term.ct0 ctid orig) idx val) = (Kind.Term.ct0 ctid orig)
+(Kind.Term.replace (Kind.Term.ct1 ctid orig x0) idx val) = (Kind.Term.ct1 ctid orig (Kind.Term.replace x0 idx val))
+(Kind.Term.replace (Kind.Term.ct2 ctid orig x0 x1) idx val) = (Kind.Term.ct2 ctid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val))
+(Kind.Term.replace (Kind.Term.ct3 ctid orig x0 x1 x2) idx val) = (Kind.Term.ct3 ctid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val))
+(Kind.Term.replace (Kind.Term.ct4 ctid orig x0 x1 x2 x3) idx val) = (Kind.Term.ct4 ctid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val))
+(Kind.Term.replace (Kind.Term.ct5 ctid orig x0 x1 x2 x3 x4) idx val) = (Kind.Term.ct5 ctid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val))
+(Kind.Term.replace (Kind.Term.ct6 ctid orig x0 x1 x2 x3 x4 x5) idx val) = (Kind.Term.ct6 ctid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val) (Kind.Term.replace x5 idx val))
+(Kind.Term.replace (Kind.Term.ct7 ctid orig args) idx val) = (Kind.Term.ct7 ctid orig (Kind.Term.replace args idx val))
+(Kind.Term.replace (Kind.Term.ct8 ctid orig args) idx val) = (Kind.Term.ct8 ctid orig (Kind.Term.replace args idx val))
+(Kind.Term.replace (Kind.Term.fn0 fnid orig) idx val) = (Kind.Term.FN0 fnid orig)
+(Kind.Term.replace (Kind.Term.fn1 fnid orig x0) idx val) = (Kind.Term.FN1 fnid orig (Kind.Term.replace x0 idx val))
+(Kind.Term.replace (Kind.Term.fn2 fnid orig x0 x1) idx val) = (Kind.Term.FN2 fnid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val))
+(Kind.Term.replace (Kind.Term.fn3 fnid orig x0 x1 x2) idx val) = (Kind.Term.FN3 fnid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val))
+(Kind.Term.replace (Kind.Term.fn4 fnid orig x0 x1 x2 x3) idx val) = (Kind.Term.FN4 fnid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val))
+(Kind.Term.replace (Kind.Term.fn5 fnid orig x0 x1 x2 x3 x4) idx val) = (Kind.Term.FN5 fnid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val))
+(Kind.Term.replace (Kind.Term.fn6 fnid orig x0 x1 x2 x3 x4 x5) idx val) = (Kind.Term.FN6 fnid orig (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val) (Kind.Term.replace x5 idx val))
+(Kind.Term.replace (Kind.Term.fn7 fnid orig args) idx val) = (Kind.Term.FN7 fnid orig (Kind.Term.replace args idx val))
+(Kind.Term.replace (Kind.Term.fn8 fnid orig args) idx val) = (Kind.Term.FN8 fnid orig (Kind.Term.replace args idx val))
+(Kind.Term.replace (Kind.Term.args7 x0 x1 x2 x3 x4 x5 x6) idx val) = (Kind.Term.args7 (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val) (Kind.Term.replace x5 idx val) (Kind.Term.replace x6 idx val))
+(Kind.Term.replace (Kind.Term.args8 x0 x1 x2 x3 x4 x5 x6 x7) idx val) = (Kind.Term.args8 (Kind.Term.replace x0 idx val) (Kind.Term.replace x1 idx val) (Kind.Term.replace x2 idx val) (Kind.Term.replace x3 idx val) (Kind.Term.replace x4 idx val) (Kind.Term.replace x5 idx val) (Kind.Term.replace x6 idx val) (Kind.Term.replace x7 idx val))
+(Kind.Term.replace (Kind.Term.hol orig numb) idx val) = (Kind.Term.hol orig numb)
+
+// Kind.Term.if_all -(res: Type) (term: (Kind.Term)) (if: (_: U60) (_: U60) (_: (Kind.Term)) (_: (_: (Kind.Term)) (Kind.Term)) res) (else: res) : res
+(Kind.Term.if_all (Kind.Term.all orig name typ body) func_if else) = ((((func_if orig) name) typ) body)
+(Kind.Term.if_all other func_if else) = else
+
 // Kind.Term.eval (term: (Kind.Term)) : (Kind.Term)
 (Kind.Term.eval (Kind.Term.typ orig)) = (Kind.Term.typ orig)
 (Kind.Term.eval (Kind.Term.var orig name index)) = (Kind.Term.var orig name index)
@@ -573,6 +716,7 @@
 (Kind.Term.eval (Kind.Term.lam orig name body)) = (Kind.Term.lam orig name @x (Kind.Term.eval (body x)))
 (Kind.Term.eval (Kind.Term.let orig name expr body)) = (Kind.Term.eval_let orig name (Kind.Term.eval expr) @x (Kind.Term.eval (body x)))
 (Kind.Term.eval (Kind.Term.ann orig expr typ)) = (Kind.Term.eval_ann orig (Kind.Term.eval expr) (Kind.Term.eval typ))
+(Kind.Term.eval (Kind.Term.sub orig name indx redx expr)) = (Kind.Term.eval_sub orig name indx redx (Kind.Term.eval expr))
 (Kind.Term.eval (Kind.Term.app orig expr typ)) = (Kind.Term.eval_app orig (Kind.Term.eval expr) (Kind.Term.eval typ))
 (Kind.Term.eval (Kind.Term.hlp orig)) = (Kind.Term.hlp orig)
 (Kind.Term.eval (Kind.Term.u60 orig)) = (Kind.Term.u60 orig)
@@ -618,119 +762,35 @@
 (Kind.Term.eval_op orig (Kind.Operator.neq) (Kind.Term.num a.orig a.num) (Kind.Term.num b.orig b.num)) = (Kind.Term.num 0 (!= a.num b.num))
 (Kind.Term.eval_op orig op left right) = (Kind.Term.op2 orig op left right)
 
-// Kind.Checker.error -(t: Type) (err: (Kind.Error)) (ret: t) : (Kind.Checker t)
-(Kind.Checker.error err ret) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked context depth rhs subst eqts (List.cons err errs) ret)
-
-// Kind.Checker.check (term: (Kind.Term)) (type: (Kind.Term)) : (Kind.Checker (Unit))
-(Kind.Checker.check (Kind.Term.lam orig name body) type) = (Kind.Checker.bind (Kind.Checker.get_subst) @subst let fun = (Kind.Term.if_all type @t_orig @t_name @t_type @t_body @orig @name @body (Kind.Checker.bind (Kind.Checker.get_depth) @dep (Kind.Checker.bind (Kind.Checker.extended (Kind.Checker.check (body (Kind.Term.var orig name dep)) (t_body (Kind.Term.var t_orig t_name dep))) name t_type (List.nil)) @chk (Kind.Checker.pure (Unit.new)))) @orig @name @body (Kind.Checker.bind (Kind.Checker.get_context) @ctx (Kind.Checker.fail (Kind.Error.cant_infer_lambda ctx orig)))); (((fun orig) name) body))
-(Kind.Checker.check (Kind.Term.let orig name expr body) type) = (Kind.Checker.bind (Kind.Checker.get_depth) @dep (Kind.Checker.bind (Kind.Checker.infer expr) @expr_typ (Kind.Checker.bind (Kind.Checker.extended (Kind.Checker.check (body (Kind.Term.var orig name dep)) type) name expr_typ (List.cons (Kind.Term.eval expr) (List.nil))) @body_chk (Kind.Checker.pure (Unit.new)))))
-(Kind.Checker.check (Kind.Term.hlp orig) type) = (Kind.Checker.bind (Kind.Checker.get_context) @ctx (Kind.Checker.bind (Kind.Checker.error (Kind.Error.inspection ctx orig type) (Unit.new)) @_ (Kind.Checker.pure (Unit.new))))
-(Kind.Checker.check (Kind.Term.var orig name idx) type) = (Kind.Checker.bind (Kind.Checker.get_right_hand_side) @rhs (Bool.if rhs (Kind.Checker.compare rhs (Kind.Term.var orig name idx) type) (Kind.Checker.extend name type (List.nil))))
-(Kind.Checker.check (Kind.Term.hol orig numb) type) = (Kind.Checker.pure (Unit.new))
-(Kind.Checker.check term type) = (Kind.Checker.bind (Kind.Checker.get_right_hand_side) @rhs (Kind.Checker.compare rhs term type))
-
-// Kind.Checker.compare (rhs: (Bool)) (term: (Kind.Term)) (type: (Kind.Term)) : (Kind.Checker (Unit))
-(Kind.Checker.compare rhs term type) = (Kind.Term.get_origin term @orig @term (Kind.Checker.bind (Kind.Checker.infer term) @term_typ let fun = (Bool.if rhs @term_typ @type (Kind.Checker.new_equation orig type term_typ) @term_typ @type (Kind.Checker.bind (Kind.Checker.equal (Kind.Term.eval term_typ) (Kind.Term.eval type)) @is_equal (Bool.if is_equal (Kind.Checker.pure (Unit.new)) (Kind.Checker.bind (Kind.Checker.get_context) @ctx (Kind.Checker.fail (Kind.Error.impossible_case ctx orig type term_typ)))))); ((fun term_typ) type)))
-
-// Kind.Term.if_all -(res: Type) (term: (Kind.Term)) (if: (_: U60) (_: U60) (_: (Kind.Term)) (_: (_: (Kind.Term)) (Kind.Term)) res) (else: res) : res
-(Kind.Term.if_all (Kind.Term.all orig name typ body) func_if else) = ((((func_if orig) name) typ) body)
-(Kind.Term.if_all other func_if else) = else
-
-// Kind.Checker.new_equation (orig: U60) (left: (Kind.Term)) (right: (Kind.Term)) : (Kind.Checker (Unit))
-(Kind.Checker.new_equation orig left right) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked context depth rhs subst (List.append eqts (Kind.Equation.new context orig left right)) errs (Unit.new))
-
-// List.append -(a: Type) (xs: (List a)) (x: a) : (List a)
-(List.append (List.nil) x) = (List.pure x)
-(List.append (List.cons xs.h xs.t) x) = (List.cons xs.h (List.append xs.t x))
-
-// Kind.Checker.get_context : (Kind.Checker (Kind.Context))
-(Kind.Checker.get_context) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked context depth rhs subst eqts errs context)
-
-// Kind.Checker.infer_args (args: (Kind.Term)) : (_: U60) (_: U60) (Kind.Term)
-(Kind.Checker.infer_args (Kind.Term.args7 x0 x1 x2 x3 x4 x5 x6)) = @ctid @orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.fn0 ctid orig) x0) x1) x2) x3) x4) x5) x6)
-(Kind.Checker.infer_args (Kind.Term.args8 x0 x1 x2 x3 x4 x5 x6 x7)) = @ctid @orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.ct0 ctid orig) x0) x1) x2) x3) x4) x5) x6) x7)
-
-// Kind.Checker.infer (term: (Kind.Term)) : (Kind.Checker (Kind.Term))
-(Kind.Checker.infer (Kind.Term.var orig name index)) = (Kind.Checker.bind (Kind.Checker.find index (Maybe.none) @n @t @v (Maybe.some t)) @got_type (Maybe.match got_type (Kind.Checker.bind (Kind.Checker.get_context) @ctx (Kind.Checker.fail (Kind.Error.unbound_variable ctx orig))) @got_type.value (Kind.Checker.pure got_type.value)))
-(Kind.Checker.infer (Kind.Term.hol orig numb)) = (Kind.Checker.bind (Kind.Checker.get_context) @ctx (Kind.Checker.fail (Kind.Error.cant_infer_hole ctx orig)))
-(Kind.Checker.infer (Kind.Term.typ orig)) = (Kind.Checker.pure (Kind.Term.typ orig))
-(Kind.Checker.infer (Kind.Term.all orig name type body)) = (Kind.Checker.bind (Kind.Checker.get_depth) @depth (Kind.Checker.bind (Kind.Checker.check type (Kind.Term.typ orig)) @_ (Kind.Checker.bind (Kind.Checker.extended (Kind.Checker.check (body (Kind.Term.var orig name depth)) (Kind.Term.typ orig)) name (Kind.Term.eval type) (List.nil)) @_ (Kind.Checker.pure (Kind.Term.typ orig)))))
-(Kind.Checker.infer (Kind.Term.lam orig name body)) = (Kind.Checker.bind (Kind.Checker.get_context) @ctx (Kind.Checker.fail (Kind.Error.cant_infer_lambda ctx orig)))
-(Kind.Checker.infer (Kind.Term.app orig func argm)) = (Kind.Checker.bind (Kind.Checker.get_subst) @subst (Kind.Checker.bind (Kind.Checker.infer func) @func_typ (Kind.Term.if_all func_typ @func_orig @func_name @func_type @func_body (Kind.Checker.bind (Kind.Checker.check argm func_type) @_ (Kind.Checker.pure (func_body (Kind.Term.eval argm)))) (Kind.Checker.bind (Kind.Checker.get_context) @ctx (Kind.Checker.fail (Kind.Error.invalid_call ctx orig))))))
-(Kind.Checker.infer (Kind.Term.let orig name expr body)) = (Kind.Checker.bind (Kind.Checker.get_depth) @dep (Kind.Checker.bind (Kind.Checker.infer expr) @expr_typ (Kind.Checker.bind (Kind.Checker.extended (Kind.Checker.infer (body (Kind.Term.var orig name dep))) name expr_typ (List.cons (Kind.Term.eval expr) (List.nil))) @body_typ (Kind.Checker.pure body_typ))))
-(Kind.Checker.infer (Kind.Term.ann orig expr type)) = let type = (Kind.Term.eval type); (Kind.Checker.bind (Kind.Checker.check expr type) @_ (Kind.Checker.pure type))
-(Kind.Checker.infer (Kind.Term.ct0 ctid orig)) = (Kind.Checker.pure (Kind.Term.eval (TypeOf ctid)))
-(Kind.Checker.infer (Kind.Term.ct1 ctid orig x0)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.ct0 ctid orig) x0))
-(Kind.Checker.infer (Kind.Term.ct2 ctid orig x0 x1)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.ct0 ctid orig) x0) x1))
-(Kind.Checker.infer (Kind.Term.ct3 ctid orig x0 x1 x2)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.ct0 ctid orig) x0) x1) x2))
-(Kind.Checker.infer (Kind.Term.ct4 ctid orig x0 x1 x2 x3)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.ct0 ctid orig) x0) x1) x2) x3))
-(Kind.Checker.infer (Kind.Term.ct5 ctid orig x0 x1 x2 x3 x4)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.ct0 ctid orig) x0) x1) x2) x3) x4))
-(Kind.Checker.infer (Kind.Term.ct6 ctid orig x0 x1 x2 x3 x4 x5)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.ct0 ctid orig) x0) x1) x2) x3) x4) x5))
-(Kind.Checker.infer (Kind.Term.ct7 ctid orig args)) = let expr = (Kind.Checker.infer_args args); (Kind.Checker.infer ((expr ctid) orig))
-(Kind.Checker.infer (Kind.Term.ct8 ctid orig args)) = let expr = (Kind.Checker.infer_args args); (Kind.Checker.infer ((expr ctid) orig))
-(Kind.Checker.infer (Kind.Term.fn0 ctid orig)) = (Kind.Checker.pure (Kind.Term.eval (TypeOf ctid)))
-(Kind.Checker.infer (Kind.Term.fn1 ctid orig x0)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.fn0 ctid orig) x0))
-(Kind.Checker.infer (Kind.Term.fn2 ctid orig x0 x1)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.fn0 ctid orig) x0) x1))
-(Kind.Checker.infer (Kind.Term.fn3 ctid orig x0 x1 x2)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.fn0 ctid orig) x0) x1) x2))
-(Kind.Checker.infer (Kind.Term.fn4 ctid orig x0 x1 x2 x3)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.fn0 ctid orig) x0) x1) x2) x3))
-(Kind.Checker.infer (Kind.Term.fn5 ctid orig x0 x1 x2 x3 x4)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.fn0 ctid orig) x0) x1) x2) x3) x4))
-(Kind.Checker.infer (Kind.Term.fn6 ctid orig x0 x1 x2 x3 x4 x5)) = (Kind.Checker.infer (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.app orig (Kind.Term.fn0 ctid orig) x0) x1) x2) x3) x4) x5))
-(Kind.Checker.infer (Kind.Term.fn7 ctid orig args)) = let expr = (Kind.Checker.infer_args args); (Kind.Checker.infer ((expr ctid) orig))
-(Kind.Checker.infer (Kind.Term.fn8 ctid orig args)) = let expr = (Kind.Checker.infer_args args); (Kind.Checker.infer ((expr ctid) orig))
-(Kind.Checker.infer (Kind.Term.hlp orig)) = (Kind.Checker.bind (Kind.Checker.get_context) @ctx (Kind.Checker.fail (Kind.Error.inspection ctx orig (Kind.Term.hlp 0))))
-(Kind.Checker.infer (Kind.Term.u60 orig)) = (Kind.Checker.pure (Kind.Term.typ 0))
-(Kind.Checker.infer (Kind.Term.num orig numb)) = (Kind.Checker.pure (Kind.Term.u60 0))
-(Kind.Checker.infer (Kind.Term.op2 orig oper left right)) = (Kind.Checker.bind (Kind.Checker.check left (Kind.Term.u60 0)) @_ (Kind.Checker.bind (Kind.Checker.check right (Kind.Term.u60 0)) @_ (Kind.Checker.pure (Kind.Term.u60 0))))
-
-// Kind.Checker.fail -(t: Type) (err: (Kind.Error)) : (Kind.Checker t)
-(Kind.Checker.fail err) = @context @depth @rhs @subst @eqts @errs (Kind.Result.errored context subst (List.cons err errs))
-
-// Kind.Term.get_origin -(r: Type) (term: (Kind.Term)) (got: (_: U60) (_: (Kind.Term)) r) : r
-(Kind.Term.get_origin (Kind.Term.typ orig) got) = ((got orig) (Kind.Term.typ orig))
-(Kind.Term.get_origin (Kind.Term.var orig name index) got) = ((got orig) (Kind.Term.var orig name index))
-(Kind.Term.get_origin (Kind.Term.hol orig numb) got) = ((got orig) (Kind.Term.hol orig numb))
-(Kind.Term.get_origin (Kind.Term.all orig name typ body) got) = ((got orig) (Kind.Term.all orig name typ body))
-(Kind.Term.get_origin (Kind.Term.lam orig name body) got) = ((got orig) (Kind.Term.lam orig name body))
-(Kind.Term.get_origin (Kind.Term.let orig name expr body) got) = ((got orig) (Kind.Term.let orig name expr body))
-(Kind.Term.get_origin (Kind.Term.ann orig expr typ) got) = ((got orig) (Kind.Term.ann orig expr typ))
-(Kind.Term.get_origin (Kind.Term.app orig func arg) got) = ((got orig) (Kind.Term.app orig func arg))
-(Kind.Term.get_origin (Kind.Term.hlp orig) got) = ((got orig) (Kind.Term.hlp orig))
-(Kind.Term.get_origin (Kind.Term.u60 orig) got) = ((got orig) (Kind.Term.u60 orig))
-(Kind.Term.get_origin (Kind.Term.num orig num) got) = ((got orig) (Kind.Term.num orig num))
-(Kind.Term.get_origin (Kind.Term.op2 orig op left right) got) = ((got orig) (Kind.Term.op2 orig op left right))
-(Kind.Term.get_origin (Kind.Term.ct0 ctid orig) got) = ((got orig) (Kind.Term.ct0 ctid orig))
-(Kind.Term.get_origin (Kind.Term.ct1 ctid orig x0) got) = ((got orig) (Kind.Term.ct1 ctid orig x0))
-(Kind.Term.get_origin (Kind.Term.ct2 ctid orig x0 x1) got) = ((got orig) (Kind.Term.ct2 ctid orig x0 x1))
-(Kind.Term.get_origin (Kind.Term.ct3 ctid orig x0 x1 x2) got) = ((got orig) (Kind.Term.ct3 ctid orig x0 x1 x2))
-(Kind.Term.get_origin (Kind.Term.ct4 ctid orig x0 x1 x2 x3) got) = ((got orig) (Kind.Term.ct4 ctid orig x0 x1 x2 x3))
-(Kind.Term.get_origin (Kind.Term.ct5 ctid orig x0 x1 x2 x3 x4) got) = ((got orig) (Kind.Term.ct5 ctid orig x0 x1 x2 x3 x4))
-(Kind.Term.get_origin (Kind.Term.ct6 ctid orig x0 x1 x2 x3 x4 x5) got) = ((got orig) (Kind.Term.ct6 ctid orig x0 x1 x2 x3 x4 x5))
-(Kind.Term.get_origin (Kind.Term.ct7 ctid orig args) got) = ((got orig) (Kind.Term.ct7 ctid orig args))
-(Kind.Term.get_origin (Kind.Term.ct8 ctid orig args) got) = ((got orig) (Kind.Term.ct8 ctid orig args))
-(Kind.Term.get_origin (Kind.Term.fn0 fnid orig) got) = ((got orig) (Kind.Term.fn0 fnid orig))
-(Kind.Term.get_origin (Kind.Term.fn1 fnid orig x0) got) = ((got orig) (Kind.Term.fn1 fnid orig x0))
-(Kind.Term.get_origin (Kind.Term.fn2 fnid orig x0 x1) got) = ((got orig) (Kind.Term.fn2 fnid orig x0 x1))
-(Kind.Term.get_origin (Kind.Term.fn3 fnid orig x0 x1 x2) got) = ((got orig) (Kind.Term.fn3 fnid orig x0 x1 x2))
-(Kind.Term.get_origin (Kind.Term.fn4 fnid orig x0 x1 x2 x3) got) = ((got orig) (Kind.Term.fn4 fnid orig x0 x1 x2 x3))
-(Kind.Term.get_origin (Kind.Term.fn5 fnid orig x0 x1 x2 x3 x4) got) = ((got orig) (Kind.Term.fn5 fnid orig x0 x1 x2 x3 x4))
-(Kind.Term.get_origin (Kind.Term.fn6 fnid orig x0 x1 x2 x3 x4 x5) got) = ((got orig) (Kind.Term.fn6 fnid orig x0 x1 x2 x3 x4 x5))
-(Kind.Term.get_origin (Kind.Term.fn7 fnid orig args) got) = ((got orig) (Kind.Term.fn7 fnid orig args))
-(Kind.Term.get_origin (Kind.Term.fn8 fnid orig args) got) = ((got orig) (Kind.Term.fn8 fnid orig args))
-
-// Kind.Checker.rule (rule: (Kind.Rule)) (term: (Kind.Term)) : (Kind.Checker (Unit))
-(Kind.Checker.rule (Kind.Rule.lhs arg args) (Kind.Term.all orig name type body)) = (Kind.Checker.bind (Kind.Checker.check arg type) @_ (Kind.Checker.bind (Kind.Checker.rule args (body arg)) @_ (Kind.Checker.pure (Unit.new))))
-(Kind.Checker.rule (Kind.Rule.lhs arg args) other) = (Kind.Checker.bind (Kind.Checker.get_context) @ctx (Kind.Checker.fail (Kind.Error.too_many_arguments ctx (Kind.Term.get_origin arg @orig @term orig))))
-(Kind.Checker.rule (Kind.Rule.rhs expr) type) = (Kind.Checker.bind (Kind.Checker.set_right_hand_side (Bool.true)) @_ (Kind.Checker.bind (Kind.Checker.check expr type) @_ (Kind.Checker.pure (Unit.new))))
-
-// Kind.Checker.set_right_hand_side (rhs: (Bool)) : (Kind.Checker (Unit))
-(Kind.Checker.set_right_hand_side to_rhs) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked context depth to_rhs subst eqts errs (Unit.new))
+// List.at.u60 -(a: Type) (xs: (List a)) (idx: U60) : (Maybe a)
+(List.at.u60 (List.nil) i) = (Maybe.none)
+(List.at.u60 (List.cons head tail) 0) = (Maybe.some head)
+(List.at.u60 (List.cons head tail) i) = (List.at.u60 tail (- i 1))
 
 // Kind.Checker.run -(t: Type) (checker: (Kind.Checker t)) (rhs: (Bool)) : (Kind.Result t)
 (Kind.Checker.run checker rhs) = ((((((checker (Kind.Context.empty)) 0) rhs) (Kind.Subst.end)) (List.nil)) (List.nil))
 
-// String.is_nil (xs: (String)) : (Bool)
-(String.is_nil "") = (Bool.true)
-(String.is_nil (String.cons x xs)) = (Bool.false)
+// Kind.Checker.unify (checker: (Kind.Checker (Unit))) : (Kind.Checker (Unit))
+(Kind.Checker.unify checker) = (Kind.Checker.bind checker @_ (Kind.Checker.bind (Kind.Checker.get_equations) @equations (Kind.Checker.unify.go equations (List.nil) (Bool.false))))
+
+// Kind.Checker.unify.go (equations: (List (Kind.Equation))) (unsolved: (List (Kind.Equation))) (changed: (Bool)) : (Kind.Checker (Unit))
+(Kind.Checker.unify.go (List.nil) (List.nil) changed) = (Kind.Checker.pure (Unit.new))
+(Kind.Checker.unify.go (List.nil) unsolved (Bool.true)) = (Kind.Checker.unify.go unsolved (List.nil) (Bool.false))
+(Kind.Checker.unify.go (List.nil) unsolved (Bool.false)) = (Kind.Checker.unify.go.fail unsolved)
+(Kind.Checker.unify.go (List.cons (Kind.Equation.new ctx orig left right) equations) unsolved changed) = (Kind.Checker.bind (Kind.Checker.with_context (Kind.Checker.equal (Kind.Term.eval left) (Kind.Term.eval right)) ctx) @is_equal let unify = (Bool.if is_equal @equations @unsolved (Kind.Checker.unify.go equations unsolved (Bool.true)) @equations @unsolved let eqt = (Kind.Equation.new ctx orig left right); (Kind.Checker.unify.go equations (List.cons eqt unsolved) changed)); ((unify equations) unsolved))
+
+// Kind.Checker.unify.go.fail (equations: (List (Kind.Equation))) : (Kind.Checker (Unit))
+(Kind.Checker.unify.go.fail (List.nil)) = (Kind.Checker.pure (Unit.new))
+(Kind.Checker.unify.go.fail (List.cons (Kind.Equation.new ctx orig left right) eqts)) = (Kind.Checker.bind (Kind.Checker.error (Kind.Error.type_mismatch ctx orig left right) (Unit.new)) @_ (Kind.Checker.unify.go.fail eqts))
+
+// Kind.Checker.with_context -(a: Type) (checker: (Kind.Checker a)) (context: (Kind.Context)) : (Kind.Checker a)
+(Kind.Checker.with_context checker new_context) = (Kind.Checker.bind (Kind.Checker.set_context new_context) @old_context (Kind.Checker.bind checker @got (Kind.Checker.bind (Kind.Checker.set_context old_context) @_ (Kind.Checker.pure got))))
+
+// Kind.Checker.set_context (new_context: (Kind.Context)) : (Kind.Checker (Kind.Context))
+(Kind.Checker.set_context new_context) = @old_context @depth @rhs @subst @eqts @errs (Kind.Result.checked new_context depth rhs subst eqts errs old_context)
+
+// Kind.Checker.get_equations : (Kind.Checker (List (Kind.Equation)))
+(Kind.Checker.get_equations) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked context depth rhs subst eqts errs eqts)
 
 // Kind.API.eval_main : (String)
 (Kind.API.eval_main) = (Kind.Printer.text (List.cons (Kind.Term.show (Kind.Term.FN0 (Main.) 0)) (List.cons (String.new_line) (List.cons (String.new_line) (List.nil)))))

src/language.rs

@@ -65,6 +65,7 @@ pub enum Term {
   App { orig: u64, func: Box<Term>, argm: Box<Term> },
   Let { orig: u64, name: String, expr: Box<Term>, body: Box<Term> },
   Ann { orig: u64, expr: Box<Term>, tipo: Box<Term> },
+  Sub { orig: u64, name: String, indx: u64, redx: u64, expr: Box<Term> },
   Ctr { orig: u64, name: String, args: Vec<Box<Term>> },
   Fun { orig: u64, name: String, args: Vec<Box<Term>> },
   Hlp { orig: u64 },
@@ -144,7 +145,7 @@ pub fn adjust_entry(book: &Book, entry: &Entry, holes: &mut u64, types: &mut Has
     args.push(Box::new(adjust_argument(book, arg, holes, &mut vars, types)?));
     vars.push(arg.name.clone());
   }
-  let tipo = Box::new(adjust_term(book, &*entry.tipo, true, holes, &mut vars, types)?);
+  let tipo = Box::new(adjust_term(book, &*entry.tipo, true, &mut 0, holes, &mut vars, types)?);
   // Adjusts each rule
   let mut rules = Vec::new();
   for rule in &entry.rules {
@@ -158,34 +159,56 @@ pub fn adjust_argument(book: &Book, arg: &Argument, holes: &mut u64, vars: &mut
   let hide = arg.hide;
   let eras = arg.eras;
   let name = arg.name.clone();
-  let tipo = Box::new(adjust_term(book, &*arg.tipo, true, holes, vars, types)?);
+  let tipo = Box::new(adjust_term(book, &*arg.tipo, true, &mut 0, holes, vars, types)?);
   return Ok(Argument { hide, eras, name, tipo });
 }
 
 pub fn adjust_rule(book: &Book, rule: &Rule, holes: &mut u64, vars: &mut Vec<String>, types: &mut HashMap<String, Rc<NewType>>) -> Result<Rule, AdjustError> {
   let name = rule.name.clone();
   let orig = rule.orig;
-  let arity = match book.entrs.get(&rule.name) {
-    Some(entry) => {
-      if rule.pats.len() != entry.args.len() {
-        return Err(AdjustError { orig, kind: AdjustErrorKind::IncorrectArity });
-      }
-    }
-    // shouldn't happen, because we only parse rules after the type annotation
-    None => {
-      panic!("Untyped rule.");
-    }
-  };
+  // shouldn't panic, because we only parse rules after the type annotation
+  let entry = book.entrs.get(&rule.name).expect("Untyped rule.");
+  let mut eras = 0;
   let mut pats = Vec::new();
   for pat in &rule.pats {
-    pats.push(Box::new(adjust_term(book, &*pat, false, holes, vars, types)?));
+    if let Term::Hol {orig, numb} = &**pat {
+      // On lhs, switch holes for vars
+      // TODO: This duplicates of adjust_term because the lhs of a rule is not a term
+      let name = format!("x{}_", eras);
+      eras = eras + 1;
+      let pat = Term::Var { orig: *orig, name };
+      pats.push(Box::new(adjust_term(book, &pat, false, &mut eras, holes, vars, types)?));
+    } else {
+      pats.push(Box::new(adjust_term(book, pat, false, &mut eras, holes, vars, types)?));
+    }
   }
-  let body = Box::new(adjust_term(book, &*rule.body, true, holes, vars, types)?);
+  // Fill erased arguments
+  let (_, eraseds) = count_implicits(entry);
+  if rule.pats.len() == entry.args.len() - eraseds {
+    pats.reverse();
+    let mut aux_pats = Vec::new();
+    for arg in &entry.args {
+      if arg.eras {
+        let name = format!("{}{}_", arg.name, eras);
+        eras = eras + 1;
+        let pat = Box::new(Term::Var { orig, name });
+        aux_pats.push(Box::new(adjust_term(book, &*pat, false, &mut eras, holes, vars, types)?));
+      } else {
+        aux_pats.push(pats.pop().unwrap());
+      }
+    }
+    pats = aux_pats;
+  }
+  if pats.len() != entry.args.len() {
+    return Err(AdjustError { orig, kind: AdjustErrorKind::IncorrectArity });
+  }
+  let body = Box::new(adjust_term(book, &*rule.body, true, &mut eras, holes, vars, types)?);
   return Ok(Rule { orig, name, pats, body });
 }
 
 // TODO: prevent defining the same name twice
-pub fn adjust_term(book: &Book, term: &Term, rhs: bool, holes: &mut u64, vars: &mut Vec<String>, types: &mut HashMap<String, Rc<NewType>>) -> Result<Term, AdjustError> {
+pub fn adjust_term(book: &Book, term: &Term, rhs: bool, eras: &mut u64, holes: &mut u64, vars: &mut Vec<String>, types: &mut HashMap<String, Rc<NewType>>) -> Result<Term, AdjustError> {
+
   fn convert_apps_to_ctr(term: &Term) -> Option<Term> {
     //println!("converting {} to ctr", show_term(term));
     let mut term = term;
@@ -232,7 +255,7 @@ pub fn adjust_term(book: &Book, term: &Term, rhs: bool, holes: &mut u64, vars: &
   }
 
   if let Some(new_term) = convert_apps_to_ctr(term) {
-    return adjust_term(book, &new_term, rhs, holes, vars, types);
+    return adjust_term(book, &new_term, rhs, eras, holes, vars, types);
   }
 
   match *term {
@@ -252,37 +275,52 @@ pub fn adjust_term(book: &Book, term: &Term, rhs: bool, holes: &mut u64, vars: &
     },
     Term::Let { ref orig, ref name, ref expr, ref body } => {
       let orig = *orig;
-      let expr = Box::new(adjust_term(book, &*expr, rhs, holes, vars, types)?);
+      let expr = Box::new(adjust_term(book, &*expr, rhs, eras, holes, vars, types)?);
       vars.push(name.clone());
-      let body = Box::new(adjust_term(book, &*body, rhs, holes, vars, types)?);
+      let body = Box::new(adjust_term(book, &*body, rhs, eras, holes, vars, types)?);
       vars.pop();
       Ok(Term::Let { orig, name: name.clone(), expr, body })
     },
     Term::Ann { ref orig, ref expr, ref tipo } => {
       let orig = *orig;
-      let expr = Box::new(adjust_term(book, &*expr, rhs, holes, vars, types)?);
-      let tipo = Box::new(adjust_term(book, &*tipo, rhs, holes, vars, types)?);
+      let expr = Box::new(adjust_term(book, &*expr, rhs, eras, holes, vars, types)?);
+      let tipo = Box::new(adjust_term(book, &*tipo, rhs, eras, holes, vars, types)?);
       Ok(Term::Ann { orig, expr, tipo })
     },
+    Term::Sub { ref orig, ref name, ref indx, ref redx, ref expr } => {
+      let orig = *orig;
+      let expr = Box::new(adjust_term(book, &*expr, rhs, eras, holes, vars, types)?);
+      match vars.iter().position(|x| x == name) {
+        None => {
+          return Err(AdjustError { orig, kind: AdjustErrorKind::UnboundVariable { name: name.clone() } });
+        }
+        Some(indx) => {
+          let name = name.clone();
+          let indx = indx as u64;
+          let redx = *redx;
+          Ok(Term::Sub { orig, name, indx, redx, expr })
+        }
+      }
+    },
     Term::All { ref orig, ref name, ref tipo, ref body } => {
       let orig = *orig;
-      let tipo = Box::new(adjust_term(book, &*tipo, rhs, holes, vars, types)?);
+      let tipo = Box::new(adjust_term(book, &*tipo, rhs, eras, holes, vars, types)?);
       vars.push(name.clone());
-      let body = Box::new(adjust_term(book, &*body, rhs, holes, vars, types)?);
+      let body = Box::new(adjust_term(book, &*body, rhs, eras, holes, vars, types)?);
       vars.pop();
       Ok(Term::All { orig, name: name.clone(), tipo, body })
     },
     Term::Lam { ref orig, ref name, ref body } => {
       let orig = *orig;
       vars.push(name.clone());
-      let body = Box::new(adjust_term(book, &*body, rhs, holes, vars, types)?);
+      let body = Box::new(adjust_term(book, &*body, rhs, eras, holes, vars, types)?);
       vars.pop();
       Ok(Term::Lam { orig, name: name.clone(), body })
     },
     Term::App { ref orig, ref func, ref argm } => {
       let orig = *orig;
-      let func = Box::new(adjust_term(book, &*func, rhs, holes, vars, types)?);
-      let argm = Box::new(adjust_term(book, &*argm, rhs, holes, vars, types)?);
+      let func = Box::new(adjust_term(book, &*func, rhs, eras, holes, vars, types)?);
+      let argm = Box::new(adjust_term(book, &*argm, rhs, eras, holes, vars, types)?);
       Ok(Term::App { orig, func, argm })
     },
     Term::Ctr { ref orig, ref name, ref args } => {
@@ -290,17 +328,19 @@ pub fn adjust_term(book: &Book, term: &Term, rhs: bool, holes: &mut u64, vars: &
       if let Some(entry) = book.entrs.get(name) {
         let mut new_args = Vec::new();
         for arg in args {
-          new_args.push(Box::new(adjust_term(book, &*arg, rhs, holes, vars, types)?));
-        }
-        // Count implicit arguments
-        let mut implicits = 0;
-        for arg in &entry.args {
-          if arg.hide {
-            implicits = implicits + 1;
+          // On lhs, switch holes for vars
+          if let (false, Term::Hol {orig, numb}) = (rhs, &**arg) {
+            let name = format!("x{}_", eras);
+            *eras = *eras + 1;
+            let arg = Box::new(Term::Var { orig: *orig, name });
+            new_args.push(Box::new(adjust_term(book, &*arg, rhs, eras, holes, vars, types)?));
+          } else {
+            new_args.push(Box::new(adjust_term(book, arg, rhs, eras, holes, vars, types)?));
           }
         }
-        // Fill implicit arguments
-        if rhs && args.len() == entry.args.len() - implicits {
+        let (hiddens, eraseds) = count_implicits(entry);
+        // Fill implicit arguments (on rhs)
+        if rhs && args.len() == entry.args.len() - hiddens {
           new_args.reverse();
           let mut aux_args = Vec::new();
           for arg in &entry.args {
@@ -314,6 +354,22 @@ pub fn adjust_term(book: &Book, term: &Term, rhs: bool, holes: &mut u64, vars: &
           }
           new_args = aux_args;
         }
+        // Fill erased arguments (on lhs)
+        if !rhs && args.len() == entry.args.len() - eraseds {
+          new_args.reverse();
+          let mut aux_args = Vec::new();
+          for arg in &entry.args {
+            if arg.eras {
+              let name = format!("{}{}_", arg.name, eras);
+              *eras = *eras + 1;
+              let arg = Term::Var { orig: orig, name };
+              aux_args.push(Box::new(adjust_term(book, &arg, rhs, eras, holes, vars, types)?));
+            } else {
+              aux_args.push(new_args.pop().unwrap());
+            }
+          }
+          new_args = aux_args;
+        }
         if new_args.len() != entry.args.len()  {
           Err(AdjustError { orig, kind: AdjustErrorKind::IncorrectArity })
         } else if entry.rules.len() > 0 {
@@ -350,8 +406,8 @@ pub fn adjust_term(book: &Book, term: &Term, rhs: bool, holes: &mut u64, vars: &
     Term::Op2 { ref orig, ref oper, ref val0, ref val1 } => {
       let orig = *orig;
       let oper = *oper;
-      let val0 = Box::new(adjust_term(book, &*val0, rhs, holes, vars, types)?);
-      let val1 = Box::new(adjust_term(book, &*val1, rhs, holes, vars, types)?);
+      let val0 = Box::new(adjust_term(book, &*val0, rhs, eras, holes, vars, types)?);
+      let val1 = Box::new(adjust_term(book, &*val1, rhs, eras, holes, vars, types)?);
       Ok(Term::Op2 { orig, oper, val0, val1 })
     },
     Term::Mat { ref orig, ref name, ref tipo, ref expr, ref cses, ref moti } => {
@@ -399,7 +455,7 @@ pub fn adjust_term(book: &Book, term: &Term, rhs: bool, holes: &mut u64, vars: &
 
         let result = Term::Ctr { orig, name: format!("{}.match", tipo), args };
         //println!("-- match desugar: {}", show_term(&result));
-        return adjust_term(book, &result, rhs, holes, vars, types);
+        return adjust_term(book, &result, rhs, eras, holes, vars, types);
 
       } else {
         return Err(AdjustError { orig, kind: AdjustErrorKind::CantLoadType });
@@ -469,6 +525,9 @@ pub fn term_get_unbounds(book: &Book, term: &Term, rhs: bool, vars: &mut Vec<Str
       term_get_unbounds(book, &*expr, rhs, vars, unbound, types);
       term_get_unbounds(book, &*tipo, rhs, vars, unbound, types);
     },
+    Term::Sub { ref name, ref expr, .. } => {
+      term_get_unbounds(book, &*expr, rhs, vars, unbound, types);
+    },
     Term::All { ref name, ref tipo, ref body, .. } => {
       term_get_unbounds(book, &*tipo, rhs, vars, unbound, types);
       vars.push(name.clone());
@@ -592,6 +651,10 @@ pub fn term_set_origin_file(term: &mut Term, file: usize) {
       term_set_origin_file(expr, file);
       term_set_origin_file(tipo, file);
     },
+    Term::Sub { ref mut orig, ref mut expr, .. } => {
+      *orig = set_origin_file(*orig, file);
+      term_set_origin_file(expr, file);
+    },
     Term::Ctr { ref mut orig, ref mut args, .. } => {
       *orig = set_origin_file(*orig, file);
       for arg in args {
@@ -641,6 +704,7 @@ pub fn get_term_origin(term: &Term) -> u64 {
     Term::App { orig, .. } => *orig,
     Term::Let { orig, .. } => *orig,
     Term::Ann { orig, .. } => *orig,
+    Term::Sub { orig, .. } => *orig,
     Term::Ctr { orig, .. } => *orig,
     Term::Fun { orig, .. } => *orig,
     Term::Hlp { orig, .. } => *orig,
@@ -1195,6 +1259,31 @@ pub fn parse_ann(state: parser::State) -> parser::Answer<Option<Box<dyn Fn(usize
     state);
 }
 
+pub fn parse_sub(state: parser::State) -> parser::Answer<Option<Box<dyn Fn(usize, Box<Term>) -> Box<Term>>>> {
+  return parser::guard(
+    parser::text_parser("##"),
+    Box::new(|state| {
+      let (state, _)    = parser::consume("##", state)?;
+      let (state, name) = parser::name1(state)?;
+      let (state, _)    = parser::consume("/", state)?;
+      let (state, redx) = parser::name1(state)?;
+      if let Ok(redx) = redx.parse::<u64>() {
+        let (state, last) = get_last_index(state)?;
+        Ok((state, Box::new(move |init, expr| {
+          let orig = origin(0, init, last);
+          let name = name.clone();
+          let indx = 0;
+          let expr = expr.clone();
+          Box::new(Term::Sub { orig, name, indx, redx, expr })
+        })))
+      } else {
+        parser::expected("number", name.len(), state)
+      }
+    }),
+    state);
+}
+
+
 pub fn parse_lst(state: parser::State) -> parser::Answer<Option<Box<Term>>> {
   parser::guard(
     Box::new(|state| {
@@ -1447,6 +1536,7 @@ pub fn parse_term_prefix(state: parser::State) -> parser::Answer<Box<Term>> {
 pub fn parse_term_suffix(state: parser::State) -> parser::Answer<Box<dyn Fn(usize,Box<Term>) -> Box<Term>>> {
   parser::grammar("Term", &[
     Box::new(parse_arr), // `->`
+    Box::new(parse_sub), // `# `
     Box::new(parse_ann), // `::`
     Box::new(|state| Ok((state, Some(Box::new(|init, term| term))))),
   ], state)
@@ -1681,6 +1771,9 @@ pub fn compile_term(term: &Term, quote: bool, lhs: bool) -> String {
     Term::Ann { orig, expr, tipo } => {
       format!("({} {} {} {})", if quote { "Kind.Term.ann" } else { "Kind.Term.eval_ann" }, hide(orig,lhs), compile_term(expr, quote, lhs), compile_term(tipo, quote, lhs))
     }
+    Term::Sub { orig, expr, name, indx, redx } => {
+      format!("({} {} {} {} {} {})", if quote { "Kind.Term.sub" } else { "Kind.Term.eval_sub" }, hide(orig,lhs), name_to_u64(name), indx, redx, compile_term(expr, quote, lhs))
+    }
     Term::Ctr { orig, name, args } => {
       let mut args_strs : Vec<String> = Vec::new();
       for arg in args {
@@ -1851,6 +1944,7 @@ pub fn compile_entry(entry: &Entry) -> String {
         return (inp, var);
       }
       _ => {
+        // TODO: This should return a proper error instead of panicking
         panic!("Invalid left-hand side pattern: {}", show_term(patt));
       }
     }
@@ -1986,7 +2080,11 @@ pub fn show_term(term: &Term) -> String {
     Term::Ann { orig: _, expr, tipo } => {
       let expr = show_term(expr);
       let tipo = show_term(tipo);
-      format!("{{{} :: {}}}", expr, tipo)
+      format!("({} :: {})", expr, tipo)
+    }
+    Term::Sub { orig: _, name, indx, redx, expr } => {
+      let expr = show_term(expr);
+      format!("{} ## {}/{}", expr, name, redx)
     }
     Term::Ctr { orig: _, name, args } => {
       format!("({}{})", name, args.iter().map(|x| format!(" {}",show_term(x))).collect::<String>())
@@ -2131,6 +2229,21 @@ pub fn u64_to_name(num: u64) -> String {
   name.chars().rev().collect()
 }
 
+/// Return the number of hidden and erased arguments in an entry
+pub fn count_implicits(entry: &Entry) -> (usize, usize) {
+  let mut hiddens = 0;
+  let mut eraseds = 0;
+  for arg in &entry.args {
+    if arg.hide {
+      hiddens = hiddens + 1;
+    }
+    if arg.eras {
+      eraseds = eraseds + 1;
+    }
+  }
+  (hiddens, eraseds)
+}
+
 // Returns true if a ctor's argument is erased
 #[derive(Clone, Debug)]
 pub enum Comp {
@@ -2178,6 +2291,9 @@ pub fn erase(book: &Book, term: &Term) -> Box<Comp> {
     Term::Ann { orig: _, expr, tipo: _ } => {
       return erase(book, expr);
     }
+    Term::Sub { orig: _, expr, name: _, indx: _, redx: _ } => {
+      return erase(book, expr);
+    }
     Term::Ctr { orig: _, name, args: term_args } => {
       let name = name.clone();
       let entr = book.entrs.get(&name).unwrap();

src/to_hvm.rs

@@ -36,6 +36,10 @@ pub fn to_hvm_term(book: &Book, term: &Term) -> String {
       let expr = to_hvm_term(book, expr);
       format!("{}", expr)
     }
+    Term::Sub { orig: _, expr, name: _, indx: _, redx: _ } => {
+      let expr = to_hvm_term(book, expr);
+      format!("{}", expr)
+    }
     Term::Ctr { orig: _, name, args } => {
       let entr = book.entrs.get(name).unwrap();
       let args = args.iter().enumerate().filter(|(i,x)| !entr.args[*i].eras).map(|x| &**x.1).collect::<Vec<&Term>>();