From 5d504fc14de4956e70213861e70e23d796c2e472 Mon Sep 17 00:00:00 2001
From: Victor Maia <victor.taelin@gmail.com>
Date: Fri, 2 Sep 2022 19:15:29 -0300
Subject: [PATCH] Rebuild

---
 bench/README.md |  61 -----
 bootstrap.sh    |   8 +-
 src/checker.hvm | 629 ++++++++++++++++++++++++------------------------
 3 files changed, 321 insertions(+), 377 deletions(-)
 delete mode 100644 bench/README.md

diff --git a/bench/README.md b/bench/README.md
deleted file mode 100644
index fbae37a9..00000000
--- a/bench/README.md
+++ /dev/null
@@ -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
-```
diff --git a/bootstrap.sh b/bootstrap.sh
index 303195e6..6d45a12d 100755
--- a/bootstrap.sh
+++ b/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
diff --git a/src/checker.hvm b/src/checker.hvm
index 4434f721..b40f4d24 100644
--- a/src/checker.hvm
+++ b/src/checker.hvm
@@ -62,6 +62,17 @@
 // 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)))))))))))))))))
 
+// 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.fill (term: (Kind.Term)) (subst: (Kind.Subst)) : (Kind.Term)
 (Kind.Term.fill term (Kind.Subst.end)) = term
 (Kind.Term.fill (Kind.Term.typ orig) sub) = (Kind.Term.typ orig)
@@ -104,10 +115,6 @@
 (Maybe.match (Maybe.none) none some) = none
 (Maybe.match (Maybe.some value_) none some) = (some value_)
 
-// 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
 
@@ -119,13 +126,9 @@
 (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.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.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.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)))))))
@@ -141,31 +144,6 @@
 // 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))
 
-// U60.to_nat (x: U60) : (Nat)
-(U60.to_nat 0) = (Nat.zero)
-(U60.to_nat n) = (Nat.succ (U60.to_nat (- n 1)))
-
-// 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)))
-
-// Kind.Name.show (name: U60) : (String)
-(Kind.Name.show name) = (Kind.Name.show.go name "")
-
-// U60.if -(r: Type) (n: U60) (t: r) (f: r) : r
-(U60.if 0 t f) = f
-(U60.if x t f) = t
-
-// 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))
-
-// Char : Type
-(Char) = 0
-
-// 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.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))))))))))
 
@@ -206,38 +184,19 @@
 (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)
-
-// Show.to_string (show: (Show)) : (String)
-(Show.to_string show) = (show "")
-
-// Show : Type
-(Show) = 0
-
-// 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.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)
-
 // 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)
 
-// 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)
+// 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)))
+
+// Kind.Name.show (name: U60) : (String)
+(Kind.Name.show name) = (Kind.Name.show.go name "")
+
+// U60.if -(r: Type) (n: U60) (t: r) (f: r) : r
+(U60.if 0 t f) = f
+(U60.if x t f) = t
 
 // Kind.Operator.show (op: (Kind.Operator)) : (String)
 (Kind.Operator.show (Kind.Operator.add)) = "+"
@@ -257,6 +216,34 @@
 (Kind.Operator.show (Kind.Operator.gtn)) = ">"
 (Kind.Operator.show (Kind.Operator.neq)) = "!="
 
+// Show.to_string (show: (Show)) : (String)
+(Show.to_string show) = (show "")
+
+// Show : Type
+(Show) = 0
+
+// Show : Type
+(Show) = 0
+
+// 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.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.pure -(a: Type) (x: a) : (Maybe a)
+(Maybe.pure x) = (Maybe.some x)
+
+// 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.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)))
@@ -271,10 +258,6 @@
 // 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)
@@ -283,6 +266,35 @@
 // List.pure -(t: Type) (x: t) : (List t)
 (List.pure x) = (List.cons x (List.nil))
 
+// String.flatten (xs: (List (String))) : (String)
+(String.flatten (List.nil)) = ""
+(String.flatten (List.cons head tail)) = (String.concat head (String.flatten tail))
+
+// 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)
+
+// String.new_line : (String)
+(String.new_line) = (String.pure (Char.newline))
+
+// String.pure (x: (Char)) : (String)
+(String.pure x) = (String.cons x "")
+
+// Char : Type
+(Char) = 0
+
+// 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)))
+
+// 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.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))
@@ -290,6 +302,10 @@
 // Kind.Context.max_name_length (ctx: (Kind.Context)) : U60
 (Kind.Context.max_name_length ctx) = (Kind.Context.max_name_length.aux ctx 0)
 
+// Nat.to_u60 (n: (Nat)) : U60
+(Nat.to_u60 (Nat.zero)) = 0
+(Nat.to_u60 (Nat.succ n)) = (+ 1 (Nat.to_u60 n))
+
 // String.length (xs: (String)) : (Nat)
 (String.length "") = (Nat.zero)
 (String.length (String.cons x xs)) = (Nat.succ (String.length xs))
@@ -297,19 +313,6 @@
 // U60.max (fst: U60) (snd: U60) : U60
 (U60.max fst snd) = (U60.if (> fst snd) fst snd)
 
-// Nat.to_u60 (n: (Nat)) : U60
-(Nat.to_u60 (Nat.zero)) = 0
-(Nat.to_u60 (Nat.succ n)) = (+ 1 (Nat.to_u60 n))
-
-// String.new_line : (String)
-(String.new_line) = (String.pure (Char.newline))
-
-// Char.newline : (Char)
-(Char.newline) = 10
-
-// String.pure (x: (Char)) : (String)
-(String.pure x) = (String.cons x "")
-
 // 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
@@ -325,16 +328,16 @@
 // 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.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)
-
 // Pair.fst -(a: Type) -(b: Type) (pair: (Pair a b)) : a
 (Pair.fst (Pair.new fst snd)) = fst
 
 // Pair.snd -(a: Type) -(b: Type) (pair: (Pair a b)) : b
 (Pair.snd (Pair.new fst snd)) = snd
 
+// 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)
+
 // List.reverse -(a: Type) (xs: (List a)) : (List a)
 (List.reverse xs) = (List.reverse.go xs (List.nil))
 
@@ -357,232 +360,6 @@
 (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.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.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.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.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 (a: Type) : Type
-(Kind.Checker a) = 0
-
-// Kind.Checker.bind.result -(a: Type) -(b: Type) (result: (Kind.Result a)) (then: (_: a) (Kind.Checker b)) : (Kind.Result b)
-(Kind.Checker.bind.result (Kind.Result.checked context depth rhs sub equations errs ret) then) = (((((((then ret) context) depth) rhs) sub) equations) errs)
-(Kind.Checker.bind.result (Kind.Result.errored context sub errs) then) = (Kind.Result.errored context sub errs)
-
-// 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.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.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)
-
-// 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.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)))))
-(Kind.Checker.equal (Kind.Term.hol a.orig a.numb) (Kind.Term.hol b.orig b.numb)) = (Bool.if (U60.equal a.numb b.numb) (Kind.Checker.pure (Bool.true)) (Kind.Checker.equal.hol a.orig a.numb (Kind.Term.hol b.orig b.numb)))
-(Kind.Checker.equal (Kind.Term.hol a.orig a.numb) b) = (Kind.Checker.equal.hol a.orig a.numb b)
-(Kind.Checker.equal b (Kind.Term.hol a.orig a.numb)) = (Kind.Checker.equal.hol a.orig a.numb b)
-(Kind.Checker.equal (Kind.Term.var a.orig a.name a.idx) b) = (Kind.Checker.bind (Kind.Checker.get_right_hand_side) @rhs (Kind.Checker.equal.var rhs a.orig a.name a.idx b))
-(Kind.Checker.equal b (Kind.Term.var a.orig a.name a.idx)) = (Kind.Checker.bind (Kind.Checker.get_right_hand_side) @rhs (Kind.Checker.equal.var rhs a.orig a.name a.idx b))
-(Kind.Checker.equal (Kind.Term.ct0 a.ctid a.orig) (Kind.Term.ct0 b.ctid b.orig)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.pure ctid)
-(Kind.Checker.equal (Kind.Term.ct1 a.ctid a.orig a.x0) (Kind.Term.ct1 b.ctid b.orig b.x0)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.pure (Bool.and ctid x0)))
-(Kind.Checker.equal (Kind.Term.ct2 a.ctid a.orig a.x0 a.x1) (Kind.Term.ct2 b.ctid b.orig b.x0 b.x1)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.bind (Kind.Checker.equal a.x1 b.x1) @x1 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 x1)))))
-(Kind.Checker.equal (Kind.Term.ct3 a.ctid a.orig a.x0 a.x1 a.x2) (Kind.Term.ct3 b.ctid b.orig b.x0 b.x1 b.x2)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.bind (Kind.Checker.equal a.x1 b.x1) @x1 (Kind.Checker.bind (Kind.Checker.equal a.x2 b.x2) @x2 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 (Bool.and x1 x2)))))))
-(Kind.Checker.equal (Kind.Term.ct4 a.ctid a.orig a.x0 a.x1 a.x2 a.x3) (Kind.Term.ct4 b.ctid b.orig b.x0 b.x1 b.x2 b.x3)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.bind (Kind.Checker.equal a.x1 b.x1) @x1 (Kind.Checker.bind (Kind.Checker.equal a.x2 b.x2) @x2 (Kind.Checker.bind (Kind.Checker.equal a.x3 b.x3) @x3 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 (Bool.and x1 (Bool.and x2 x3)))))))))
-(Kind.Checker.equal (Kind.Term.ct5 a.ctid a.orig a.x0 a.x1 a.x2 a.x3 a.x4) (Kind.Term.ct5 b.ctid b.orig b.x0 b.x1 b.x2 b.x3 b.x4)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.bind (Kind.Checker.equal a.x1 b.x1) @x1 (Kind.Checker.bind (Kind.Checker.equal a.x2 b.x2) @x2 (Kind.Checker.bind (Kind.Checker.equal a.x3 b.x3) @x3 (Kind.Checker.bind (Kind.Checker.equal a.x4 b.x4) @x4 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 x4)))))))))))
-(Kind.Checker.equal (Kind.Term.ct6 a.ctid a.orig a.x0 a.x1 a.x2 a.x3 a.x4 a.x5) (Kind.Term.ct6 b.ctid b.orig b.x0 b.x1 b.x2 b.x3 b.x4 b.x5)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.bind (Kind.Checker.equal a.x1 b.x1) @x1 (Kind.Checker.bind (Kind.Checker.equal a.x2 b.x2) @x2 (Kind.Checker.bind (Kind.Checker.equal a.x3 b.x3) @x3 (Kind.Checker.bind (Kind.Checker.equal a.x4 b.x4) @x4 (Kind.Checker.bind (Kind.Checker.equal a.x5 b.x5) @x5 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 x5)))))))))))))
-(Kind.Checker.equal (Kind.Term.ct7 a.ctid a.orig a.args) (Kind.Term.ct7 b.ctid b.orig b.args)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.args b.args) @xargs (Kind.Checker.pure (Bool.and ctid xargs)))
-(Kind.Checker.equal (Kind.Term.ct8 a.ctid a.orig a.args) (Kind.Term.ct8 b.ctid b.orig b.args)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.args b.args) @xargs (Kind.Checker.pure (Bool.and ctid xargs)))
-(Kind.Checker.equal (Kind.Term.args7 a.x0 a.x1 a.x2 a.x3 a.x4 a.x5 a.x6) (Kind.Term.args7 b.x0 b.x1 b.x2 b.x3 b.x4 b.x5 b.x6)) = (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.bind (Kind.Checker.equal a.x1 b.x1) @x1 (Kind.Checker.bind (Kind.Checker.equal a.x2 b.x2) @x2 (Kind.Checker.bind (Kind.Checker.equal a.x3 b.x3) @x3 (Kind.Checker.bind (Kind.Checker.equal a.x4 b.x4) @x4 (Kind.Checker.bind (Kind.Checker.equal a.x5 b.x5) @x5 (Kind.Checker.bind (Kind.Checker.equal a.x6 b.x6) @x6 (Kind.Checker.pure (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 (Bool.and x5 x6))))))))))))))
-(Kind.Checker.equal (Kind.Term.args8 a.x0 a.x1 a.x2 a.x3 a.x4 a.x5 a.x6 a.x7) (Kind.Term.args8 b.x0 b.x1 b.x2 b.x3 b.x4 b.x5 b.x6 b.x7)) = (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.bind (Kind.Checker.equal a.x1 b.x1) @x1 (Kind.Checker.bind (Kind.Checker.equal a.x2 b.x2) @x2 (Kind.Checker.bind (Kind.Checker.equal a.x3 b.x3) @x3 (Kind.Checker.bind (Kind.Checker.equal a.x4 b.x4) @x4 (Kind.Checker.bind (Kind.Checker.equal a.x5 b.x5) @x5 (Kind.Checker.bind (Kind.Checker.equal a.x6 b.x6) @x6 (Kind.Checker.bind (Kind.Checker.equal a.x7 b.x7) @x7 (Kind.Checker.pure (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 (Bool.and x5 (Bool.and x6 x7))))))))))))))))
-(Kind.Checker.equal (Kind.Term.fn0 a.ctid a.orig) (Kind.Term.fn0 b.ctid b.orig)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.pure ctid)
-(Kind.Checker.equal (Kind.Term.fn1 a.ctid a.orig a.x0) (Kind.Term.fn1 b.ctid b.orig b.x0)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.pure (Bool.and ctid x0)))
-(Kind.Checker.equal (Kind.Term.fn2 a.ctid a.orig a.x0 a.x1) (Kind.Term.fn2 b.ctid b.orig b.x0 b.x1)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.bind (Kind.Checker.equal a.x1 b.x1) @x1 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 x1)))))
-(Kind.Checker.equal (Kind.Term.fn3 a.ctid a.orig a.x0 a.x1 a.x2) (Kind.Term.fn3 b.ctid b.orig b.x0 b.x1 b.x2)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.bind (Kind.Checker.equal a.x1 b.x1) @x1 (Kind.Checker.bind (Kind.Checker.equal a.x2 b.x2) @x2 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 (Bool.and x1 x2)))))))
-(Kind.Checker.equal (Kind.Term.fn4 a.ctid a.orig a.x0 a.x1 a.x2 a.x3) (Kind.Term.fn4 b.ctid b.orig b.x0 b.x1 b.x2 b.x3)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.bind (Kind.Checker.equal a.x1 b.x1) @x1 (Kind.Checker.bind (Kind.Checker.equal a.x2 b.x2) @x2 (Kind.Checker.bind (Kind.Checker.equal a.x3 b.x3) @x3 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 (Bool.and x1 (Bool.and x2 x3)))))))))
-(Kind.Checker.equal (Kind.Term.fn5 a.ctid a.orig a.x0 a.x1 a.x2 a.x3 a.x4) (Kind.Term.fn5 b.ctid b.orig b.x0 b.x1 b.x2 b.x3 b.x4)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.bind (Kind.Checker.equal a.x1 b.x1) @x1 (Kind.Checker.bind (Kind.Checker.equal a.x2 b.x2) @x2 (Kind.Checker.bind (Kind.Checker.equal a.x3 b.x3) @x3 (Kind.Checker.bind (Kind.Checker.equal a.x4 b.x4) @x4 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 x4)))))))))))
-(Kind.Checker.equal (Kind.Term.fn6 a.ctid a.orig a.x0 a.x1 a.x2 a.x3 a.x4 a.x5) (Kind.Term.fn6 b.ctid b.orig b.x0 b.x1 b.x2 b.x3 b.x4 b.x5)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.bind (Kind.Checker.equal a.x1 b.x1) @x1 (Kind.Checker.bind (Kind.Checker.equal a.x2 b.x2) @x2 (Kind.Checker.bind (Kind.Checker.equal a.x3 b.x3) @x3 (Kind.Checker.bind (Kind.Checker.equal a.x4 b.x4) @x4 (Kind.Checker.bind (Kind.Checker.equal a.x5 b.x5) @x5 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 x5)))))))))))))
-(Kind.Checker.equal (Kind.Term.fn7 a.ctid a.orig a.args) (Kind.Term.fn7 b.ctid b.orig b.args)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.args b.args) @xargs (Kind.Checker.pure (Bool.and ctid xargs)))
-(Kind.Checker.equal (Kind.Term.fn8 a.ctid a.orig a.args) (Kind.Term.fn8 b.ctid b.orig b.args)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.args b.args) @xargs (Kind.Checker.pure (Bool.and ctid xargs)))
-(Kind.Checker.equal a b) = (Kind.Checker.bind (Kind.Checker.get_subst) @sub (Bool.if (Bool.or (Kind.Term.fillable a sub) (Kind.Term.fillable b sub)) (Kind.Checker.equal (Kind.Term.fill a sub) (Kind.Term.fill b sub)) (Kind.Checker.pure (Bool.false))))
-
-// Kind.Checker.equal.var (rhs: (Bool)) (orig: U60) (name: U60) (idx: U60) (b: (Kind.Term)) : (Kind.Checker (Bool))
-(Kind.Checker.equal.var (Bool.false) orig name idx b) = (Kind.Checker.bind (Kind.Checker.add_value idx b) @_ (Kind.Checker.pure (Bool.true)))
-(Kind.Checker.equal.var (Bool.true) a.orig a.name a.idx (Kind.Term.var b.orig b.name b.idx)) = (Bool.if (U60.equal a.idx b.idx) (Kind.Checker.pure (Bool.true)) (Kind.Checker.bind (Kind.Checker.find a.idx (List.nil) @n @t @v v) @a.val (Kind.Checker.bind (Kind.Checker.find b.idx (List.nil) @n @t @v v) @b.val (Kind.Checker.bind (Kind.Checker.equal.var.try_values a.val (Kind.Term.var b.orig b.name b.idx)) @a.chk (Kind.Checker.bind (Kind.Checker.equal.var.try_values b.val (Kind.Term.var a.orig a.name a.idx)) @b.chk (Kind.Checker.pure (Bool.or a.chk b.chk)))))))
-(Kind.Checker.equal.var (Bool.true) a.orig a.name a.idx b) = (Kind.Checker.bind (Kind.Checker.get_subst) @sub (Bool.if (Kind.Term.fillable b sub) (Kind.Checker.equal (Kind.Term.var a.orig a.name a.idx) (Kind.Term.fill b sub)) (Kind.Checker.bind (Kind.Checker.find a.idx (List.nil) @n @t @v v) @a.val (Kind.Checker.bind (Kind.Checker.equal.var.try_values a.val b) @res (Kind.Checker.pure res)))))
-
-// Kind.Checker.equal.var.try_values (ls: (List (Kind.Term))) (term: (Kind.Term)) : (Kind.Checker (Bool))
-(Kind.Checker.equal.var.try_values (List.nil) term) = (Kind.Checker.pure (Bool.false))
-(Kind.Checker.equal.var.try_values (List.cons x xs) term) = (Kind.Checker.bind (Kind.Checker.equal x term) @head (Bool.if head (Kind.Checker.pure (Bool.true)) (Kind.Checker.equal.var.try_values xs term)))
-
-// Kind.Checker.equal.hol (orig: U60) (numb: U60) (b: (Kind.Term)) : (Kind.Checker (Bool))
-(Kind.Checker.equal.hol a.orig a.numb b) = (Kind.Checker.bind (Kind.Checker.look a.numb) @got (Kind.Checker.bind (Kind.Checker.equal.hol.val got a.orig a.numb b) @res (Kind.Checker.pure res)))
-
-// Kind.Checker.equal.hol.val (val: (Maybe (Kind.Term))) (orig: U60) (numb: U60) (b: (Kind.Term)) : (Kind.Checker (Bool))
-(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.get_right_hand_side : (Kind.Checker (Bool))
-(Kind.Checker.get_right_hand_side) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked context depth rhs subst eqts errs rhs)
-
-// 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.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))
-
-// Bool.or (a: (Bool)) (b: (Bool)) : (Bool)
-(Bool.or (Bool.true) b) = (Bool.true)
-(Bool.or (Bool.false) b) = b
-
-// 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)
-(Kind.Term.fillable (Kind.Term.var orig name index) sub) = (Bool.false)
-(Kind.Term.fillable (Kind.Term.hlp orig) sub) = (Bool.false)
-(Kind.Term.fillable (Kind.Term.u60 orig) sub) = (Bool.false)
-(Kind.Term.fillable (Kind.Term.num orig num) sub) = (Bool.false)
-(Kind.Term.fillable (Kind.Term.all orig name typ body) sub) = (Bool.or (Kind.Term.fillable typ sub) (Kind.Term.fillable (body (Kind.Term.hlp 0)) sub))
-(Kind.Term.fillable (Kind.Term.lam orig name body) sub) = (Kind.Term.fillable (body (Kind.Term.hlp 0)) sub)
-(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.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)
-(Kind.Term.fillable (Kind.Term.ct1 ctid orig x0) sub) = (Kind.Term.fillable x0 sub)
-(Kind.Term.fillable (Kind.Term.ct2 ctid orig x0 x1) sub) = (Bool.or (Kind.Term.fillable x0 sub) (Kind.Term.fillable x1 sub))
-(Kind.Term.fillable (Kind.Term.ct3 ctid orig x0 x1 x2) sub) = (Bool.or (Kind.Term.fillable x0 sub) (Bool.or (Kind.Term.fillable x1 sub) (Kind.Term.fillable x2 sub)))
-(Kind.Term.fillable (Kind.Term.ct4 ctid orig x0 x1 x2 x3) sub) = (Bool.or (Kind.Term.fillable x0 sub) (Bool.or (Kind.Term.fillable x1 sub) (Bool.or (Kind.Term.fillable x2 sub) (Kind.Term.fillable x3 sub))))
-(Kind.Term.fillable (Kind.Term.ct5 ctid orig x0 x1 x2 x3 x4) 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) (Kind.Term.fillable x4 sub)))))
-(Kind.Term.fillable (Kind.Term.ct6 ctid orig x0 x1 x2 x3 x4 x5) 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) (Kind.Term.fillable x5 sub))))))
-(Kind.Term.fillable (Kind.Term.ct7 fnid orig args) sub) = (Kind.Term.fillable args sub)
-(Kind.Term.fillable (Kind.Term.ct8 fnid orig args) sub) = (Kind.Term.fillable args sub)
-(Kind.Term.fillable (Kind.Term.fn0 fnid orig) sub) = (Bool.false)
-(Kind.Term.fillable (Kind.Term.fn1 fnid orig x0) sub) = (Kind.Term.fillable x0 sub)
-(Kind.Term.fillable (Kind.Term.fn2 fnid orig x0 x1) sub) = (Bool.or (Kind.Term.fillable x0 sub) (Kind.Term.fillable x1 sub))
-(Kind.Term.fillable (Kind.Term.fn3 fnid orig x0 x1 x2) sub) = (Bool.or (Kind.Term.fillable x0 sub) (Bool.or (Kind.Term.fillable x1 sub) (Kind.Term.fillable x2 sub)))
-(Kind.Term.fillable (Kind.Term.fn4 fnid orig x0 x1 x2 x3) sub) = (Bool.or (Kind.Term.fillable x0 sub) (Bool.or (Kind.Term.fillable x1 sub) (Bool.or (Kind.Term.fillable x2 sub) (Kind.Term.fillable x3 sub))))
-(Kind.Term.fillable (Kind.Term.fn5 fnid orig x0 x1 x2 x3 x4) 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) (Kind.Term.fillable x4 sub)))))
-(Kind.Term.fillable (Kind.Term.fn6 fnid orig x0 x1 x2 x3 x4 x5) 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) (Kind.Term.fillable x5 sub))))))
-(Kind.Term.fillable (Kind.Term.fn7 fnid orig args) sub) = (Kind.Term.fillable args sub)
-(Kind.Term.fillable (Kind.Term.fn8 fnid orig args) sub) = (Kind.Term.fillable args sub)
-(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))))))))
-
-// 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.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.Operator.equal (left: (Kind.Operator)) (right: (Kind.Operator)) : (Bool)
-(Kind.Operator.equal (Kind.Operator.and) (Kind.Operator.and)) = (Bool.true)
-(Kind.Operator.equal (Kind.Operator.sub) (Kind.Operator.sub)) = (Bool.true)
-(Kind.Operator.equal (Kind.Operator.mul) (Kind.Operator.mul)) = (Bool.true)
-(Kind.Operator.equal (Kind.Operator.div) (Kind.Operator.div)) = (Bool.true)
-(Kind.Operator.equal (Kind.Operator.mod) (Kind.Operator.mod)) = (Bool.true)
-(Kind.Operator.equal (Kind.Operator.and) (Kind.Operator.and)) = (Bool.true)
-(Kind.Operator.equal (Kind.Operator.or) (Kind.Operator.or)) = (Bool.true)
-(Kind.Operator.equal (Kind.Operator.xor) (Kind.Operator.xor)) = (Bool.true)
-(Kind.Operator.equal (Kind.Operator.shl) (Kind.Operator.shl)) = (Bool.true)
-(Kind.Operator.equal (Kind.Operator.shr) (Kind.Operator.shr)) = (Bool.true)
-(Kind.Operator.equal (Kind.Operator.ltn) (Kind.Operator.ltn)) = (Bool.true)
-(Kind.Operator.equal (Kind.Operator.lte) (Kind.Operator.lte)) = (Bool.true)
-(Kind.Operator.equal (Kind.Operator.eql) (Kind.Operator.eql)) = (Bool.true)
-(Kind.Operator.equal (Kind.Operator.gte) (Kind.Operator.gte)) = (Bool.true)
-(Kind.Operator.equal (Kind.Operator.gtn) (Kind.Operator.gtn)) = (Bool.true)
-(Kind.Operator.equal (Kind.Operator.neq) (Kind.Operator.neq)) = (Bool.true)
-(Kind.Operator.equal a b) = (Bool.false)
-
-// U60.equal (a: U60) (b: U60) : (Bool)
-(U60.equal a b) = (U60.to_bool (== a b))
-
-// U60.to_bool (n: U60) : (Bool)
-(U60.to_bool 0) = (Bool.false)
-(U60.to_bool n) = (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)
-
-// Bool.and (a: (Bool)) (b: (Bool)) : (Bool)
-(Bool.and (Bool.true) b) = b
-(Bool.and (Bool.false) b) = (Bool.false)
-
-// 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.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.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)
@@ -636,6 +413,27 @@
 (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.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.bind.result -(a: Type) -(b: Type) (result: (Kind.Result a)) (then: (_: a) (Kind.Checker b)) : (Kind.Result b)
+(Kind.Checker.bind.result (Kind.Result.checked context depth rhs sub equations errs ret) then) = (((((((then ret) context) depth) rhs) sub) equations) errs)
+(Kind.Checker.bind.result (Kind.Result.errored context sub errs) then) = (Kind.Result.errored context sub errs)
+
+// 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.Checker (a: Type) : Type
+(Kind.Checker a) = 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.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.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))
@@ -668,12 +466,61 @@
 (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.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.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.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.get_right_hand_side : (Kind.Checker (Bool))
+(Kind.Checker.get_right_hand_side) = @context @depth @rhs @subst @eqts @errs (Kind.Result.checked context depth rhs subst eqts errs rhs)
+
+// 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.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.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.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.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.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)
+
 // 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)
@@ -710,8 +557,164 @@
 (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.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.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.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.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.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)))))
+(Kind.Checker.equal (Kind.Term.hol a.orig a.numb) (Kind.Term.hol b.orig b.numb)) = (Bool.if (U60.equal a.numb b.numb) (Kind.Checker.pure (Bool.true)) (Kind.Checker.equal.hol a.orig a.numb (Kind.Term.hol b.orig b.numb)))
+(Kind.Checker.equal (Kind.Term.hol a.orig a.numb) b) = (Kind.Checker.equal.hol a.orig a.numb b)
+(Kind.Checker.equal b (Kind.Term.hol a.orig a.numb)) = (Kind.Checker.equal.hol a.orig a.numb b)
+(Kind.Checker.equal (Kind.Term.var a.orig a.name a.idx) b) = (Kind.Checker.bind (Kind.Checker.get_right_hand_side) @rhs (Kind.Checker.equal.var rhs a.orig a.name a.idx b))
+(Kind.Checker.equal b (Kind.Term.var a.orig a.name a.idx)) = (Kind.Checker.bind (Kind.Checker.get_right_hand_side) @rhs (Kind.Checker.equal.var rhs a.orig a.name a.idx b))
+(Kind.Checker.equal (Kind.Term.ct0 a.ctid a.orig) (Kind.Term.ct0 b.ctid b.orig)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.pure ctid)
+(Kind.Checker.equal (Kind.Term.ct1 a.ctid a.orig a.x0) (Kind.Term.ct1 b.ctid b.orig b.x0)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.pure (Bool.and ctid x0)))
+(Kind.Checker.equal (Kind.Term.ct2 a.ctid a.orig a.x0 a.x1) (Kind.Term.ct2 b.ctid b.orig b.x0 b.x1)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.bind (Kind.Checker.equal a.x1 b.x1) @x1 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 x1)))))
+(Kind.Checker.equal (Kind.Term.ct3 a.ctid a.orig a.x0 a.x1 a.x2) (Kind.Term.ct3 b.ctid b.orig b.x0 b.x1 b.x2)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.bind (Kind.Checker.equal a.x1 b.x1) @x1 (Kind.Checker.bind (Kind.Checker.equal a.x2 b.x2) @x2 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 (Bool.and x1 x2)))))))
+(Kind.Checker.equal (Kind.Term.ct4 a.ctid a.orig a.x0 a.x1 a.x2 a.x3) (Kind.Term.ct4 b.ctid b.orig b.x0 b.x1 b.x2 b.x3)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.bind (Kind.Checker.equal a.x1 b.x1) @x1 (Kind.Checker.bind (Kind.Checker.equal a.x2 b.x2) @x2 (Kind.Checker.bind (Kind.Checker.equal a.x3 b.x3) @x3 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 (Bool.and x1 (Bool.and x2 x3)))))))))
+(Kind.Checker.equal (Kind.Term.ct5 a.ctid a.orig a.x0 a.x1 a.x2 a.x3 a.x4) (Kind.Term.ct5 b.ctid b.orig b.x0 b.x1 b.x2 b.x3 b.x4)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.bind (Kind.Checker.equal a.x1 b.x1) @x1 (Kind.Checker.bind (Kind.Checker.equal a.x2 b.x2) @x2 (Kind.Checker.bind (Kind.Checker.equal a.x3 b.x3) @x3 (Kind.Checker.bind (Kind.Checker.equal a.x4 b.x4) @x4 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 x4)))))))))))
+(Kind.Checker.equal (Kind.Term.ct6 a.ctid a.orig a.x0 a.x1 a.x2 a.x3 a.x4 a.x5) (Kind.Term.ct6 b.ctid b.orig b.x0 b.x1 b.x2 b.x3 b.x4 b.x5)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.bind (Kind.Checker.equal a.x1 b.x1) @x1 (Kind.Checker.bind (Kind.Checker.equal a.x2 b.x2) @x2 (Kind.Checker.bind (Kind.Checker.equal a.x3 b.x3) @x3 (Kind.Checker.bind (Kind.Checker.equal a.x4 b.x4) @x4 (Kind.Checker.bind (Kind.Checker.equal a.x5 b.x5) @x5 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 x5)))))))))))))
+(Kind.Checker.equal (Kind.Term.ct7 a.ctid a.orig a.args) (Kind.Term.ct7 b.ctid b.orig b.args)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.args b.args) @xargs (Kind.Checker.pure (Bool.and ctid xargs)))
+(Kind.Checker.equal (Kind.Term.ct8 a.ctid a.orig a.args) (Kind.Term.ct8 b.ctid b.orig b.args)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.args b.args) @xargs (Kind.Checker.pure (Bool.and ctid xargs)))
+(Kind.Checker.equal (Kind.Term.args7 a.x0 a.x1 a.x2 a.x3 a.x4 a.x5 a.x6) (Kind.Term.args7 b.x0 b.x1 b.x2 b.x3 b.x4 b.x5 b.x6)) = (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.bind (Kind.Checker.equal a.x1 b.x1) @x1 (Kind.Checker.bind (Kind.Checker.equal a.x2 b.x2) @x2 (Kind.Checker.bind (Kind.Checker.equal a.x3 b.x3) @x3 (Kind.Checker.bind (Kind.Checker.equal a.x4 b.x4) @x4 (Kind.Checker.bind (Kind.Checker.equal a.x5 b.x5) @x5 (Kind.Checker.bind (Kind.Checker.equal a.x6 b.x6) @x6 (Kind.Checker.pure (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 (Bool.and x5 x6))))))))))))))
+(Kind.Checker.equal (Kind.Term.args8 a.x0 a.x1 a.x2 a.x3 a.x4 a.x5 a.x6 a.x7) (Kind.Term.args8 b.x0 b.x1 b.x2 b.x3 b.x4 b.x5 b.x6 b.x7)) = (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.bind (Kind.Checker.equal a.x1 b.x1) @x1 (Kind.Checker.bind (Kind.Checker.equal a.x2 b.x2) @x2 (Kind.Checker.bind (Kind.Checker.equal a.x3 b.x3) @x3 (Kind.Checker.bind (Kind.Checker.equal a.x4 b.x4) @x4 (Kind.Checker.bind (Kind.Checker.equal a.x5 b.x5) @x5 (Kind.Checker.bind (Kind.Checker.equal a.x6 b.x6) @x6 (Kind.Checker.bind (Kind.Checker.equal a.x7 b.x7) @x7 (Kind.Checker.pure (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 (Bool.and x5 (Bool.and x6 x7))))))))))))))))
+(Kind.Checker.equal (Kind.Term.fn0 a.ctid a.orig) (Kind.Term.fn0 b.ctid b.orig)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.pure ctid)
+(Kind.Checker.equal (Kind.Term.fn1 a.ctid a.orig a.x0) (Kind.Term.fn1 b.ctid b.orig b.x0)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.pure (Bool.and ctid x0)))
+(Kind.Checker.equal (Kind.Term.fn2 a.ctid a.orig a.x0 a.x1) (Kind.Term.fn2 b.ctid b.orig b.x0 b.x1)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.bind (Kind.Checker.equal a.x1 b.x1) @x1 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 x1)))))
+(Kind.Checker.equal (Kind.Term.fn3 a.ctid a.orig a.x0 a.x1 a.x2) (Kind.Term.fn3 b.ctid b.orig b.x0 b.x1 b.x2)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.bind (Kind.Checker.equal a.x1 b.x1) @x1 (Kind.Checker.bind (Kind.Checker.equal a.x2 b.x2) @x2 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 (Bool.and x1 x2)))))))
+(Kind.Checker.equal (Kind.Term.fn4 a.ctid a.orig a.x0 a.x1 a.x2 a.x3) (Kind.Term.fn4 b.ctid b.orig b.x0 b.x1 b.x2 b.x3)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.bind (Kind.Checker.equal a.x1 b.x1) @x1 (Kind.Checker.bind (Kind.Checker.equal a.x2 b.x2) @x2 (Kind.Checker.bind (Kind.Checker.equal a.x3 b.x3) @x3 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 (Bool.and x1 (Bool.and x2 x3)))))))))
+(Kind.Checker.equal (Kind.Term.fn5 a.ctid a.orig a.x0 a.x1 a.x2 a.x3 a.x4) (Kind.Term.fn5 b.ctid b.orig b.x0 b.x1 b.x2 b.x3 b.x4)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.bind (Kind.Checker.equal a.x1 b.x1) @x1 (Kind.Checker.bind (Kind.Checker.equal a.x2 b.x2) @x2 (Kind.Checker.bind (Kind.Checker.equal a.x3 b.x3) @x3 (Kind.Checker.bind (Kind.Checker.equal a.x4 b.x4) @x4 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 x4)))))))))))
+(Kind.Checker.equal (Kind.Term.fn6 a.ctid a.orig a.x0 a.x1 a.x2 a.x3 a.x4 a.x5) (Kind.Term.fn6 b.ctid b.orig b.x0 b.x1 b.x2 b.x3 b.x4 b.x5)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.x0 b.x0) @x0 (Kind.Checker.bind (Kind.Checker.equal a.x1 b.x1) @x1 (Kind.Checker.bind (Kind.Checker.equal a.x2 b.x2) @x2 (Kind.Checker.bind (Kind.Checker.equal a.x3 b.x3) @x3 (Kind.Checker.bind (Kind.Checker.equal a.x4 b.x4) @x4 (Kind.Checker.bind (Kind.Checker.equal a.x5 b.x5) @x5 (Kind.Checker.pure (Bool.and ctid (Bool.and x0 (Bool.and x1 (Bool.and x2 (Bool.and x3 (Bool.and x4 x5)))))))))))))
+(Kind.Checker.equal (Kind.Term.fn7 a.ctid a.orig a.args) (Kind.Term.fn7 b.ctid b.orig b.args)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.args b.args) @xargs (Kind.Checker.pure (Bool.and ctid xargs)))
+(Kind.Checker.equal (Kind.Term.fn8 a.ctid a.orig a.args) (Kind.Term.fn8 b.ctid b.orig b.args)) = let ctid = (U60.equal (HashOf a.ctid) (HashOf b.ctid)); (Kind.Checker.bind (Kind.Checker.equal a.args b.args) @xargs (Kind.Checker.pure (Bool.and ctid xargs)))
+(Kind.Checker.equal a b) = (Kind.Checker.bind (Kind.Checker.get_subst) @sub (Bool.if (Bool.or (Kind.Term.fillable a sub) (Kind.Term.fillable b sub)) (Kind.Checker.equal (Kind.Term.fill a sub) (Kind.Term.fill b sub)) (Kind.Checker.pure (Bool.false))))
+
+// Kind.Checker.equal.var (rhs: (Bool)) (orig: U60) (name: U60) (idx: U60) (b: (Kind.Term)) : (Kind.Checker (Bool))
+(Kind.Checker.equal.var (Bool.false) orig name idx b) = (Kind.Checker.bind (Kind.Checker.add_value idx b) @_ (Kind.Checker.pure (Bool.true)))
+(Kind.Checker.equal.var (Bool.true) a.orig a.name a.idx (Kind.Term.var b.orig b.name b.idx)) = (Bool.if (U60.equal a.idx b.idx) (Kind.Checker.pure (Bool.true)) (Kind.Checker.bind (Kind.Checker.find a.idx (List.nil) @n @t @v v) @a.val (Kind.Checker.bind (Kind.Checker.find b.idx (List.nil) @n @t @v v) @b.val (Kind.Checker.bind (Kind.Checker.equal.var.try_values a.val (Kind.Term.var b.orig b.name b.idx)) @a.chk (Kind.Checker.bind (Kind.Checker.equal.var.try_values b.val (Kind.Term.var a.orig a.name a.idx)) @b.chk (Kind.Checker.pure (Bool.or a.chk b.chk)))))))
+(Kind.Checker.equal.var (Bool.true) a.orig a.name a.idx b) = (Kind.Checker.bind (Kind.Checker.get_subst) @sub (Bool.if (Kind.Term.fillable b sub) (Kind.Checker.equal (Kind.Term.var a.orig a.name a.idx) (Kind.Term.fill b sub)) (Kind.Checker.bind (Kind.Checker.find a.idx (List.nil) @n @t @v v) @a.val (Kind.Checker.bind (Kind.Checker.equal.var.try_values a.val b) @res (Kind.Checker.pure res)))))
+
+// Kind.Checker.equal.var.try_values (ls: (List (Kind.Term))) (term: (Kind.Term)) : (Kind.Checker (Bool))
+(Kind.Checker.equal.var.try_values (List.nil) term) = (Kind.Checker.pure (Bool.false))
+(Kind.Checker.equal.var.try_values (List.cons x xs) term) = (Kind.Checker.bind (Kind.Checker.equal x term) @head (Bool.if head (Kind.Checker.pure (Bool.true)) (Kind.Checker.equal.var.try_values xs term)))
+
+// Kind.Checker.equal.hol (orig: U60) (numb: U60) (b: (Kind.Term)) : (Kind.Checker (Bool))
+(Kind.Checker.equal.hol a.orig a.numb b) = (Kind.Checker.bind (Kind.Checker.look a.numb) @got (Kind.Checker.bind (Kind.Checker.equal.hol.val got a.orig a.numb b) @res (Kind.Checker.pure res)))
+
+// Kind.Checker.equal.hol.val (val: (Maybe (Kind.Term))) (orig: U60) (numb: U60) (b: (Kind.Term)) : (Kind.Checker (Bool))
+(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.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.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)
+(Kind.Term.fillable (Kind.Term.var orig name index) sub) = (Bool.false)
+(Kind.Term.fillable (Kind.Term.hlp orig) sub) = (Bool.false)
+(Kind.Term.fillable (Kind.Term.u60 orig) sub) = (Bool.false)
+(Kind.Term.fillable (Kind.Term.num orig num) sub) = (Bool.false)
+(Kind.Term.fillable (Kind.Term.all orig name typ body) sub) = (Bool.or (Kind.Term.fillable typ sub) (Kind.Term.fillable (body (Kind.Term.hlp 0)) sub))
+(Kind.Term.fillable (Kind.Term.lam orig name body) sub) = (Kind.Term.fillable (body (Kind.Term.hlp 0)) sub)
+(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.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)
+(Kind.Term.fillable (Kind.Term.ct1 ctid orig x0) sub) = (Kind.Term.fillable x0 sub)
+(Kind.Term.fillable (Kind.Term.ct2 ctid orig x0 x1) sub) = (Bool.or (Kind.Term.fillable x0 sub) (Kind.Term.fillable x1 sub))
+(Kind.Term.fillable (Kind.Term.ct3 ctid orig x0 x1 x2) sub) = (Bool.or (Kind.Term.fillable x0 sub) (Bool.or (Kind.Term.fillable x1 sub) (Kind.Term.fillable x2 sub)))
+(Kind.Term.fillable (Kind.Term.ct4 ctid orig x0 x1 x2 x3) sub) = (Bool.or (Kind.Term.fillable x0 sub) (Bool.or (Kind.Term.fillable x1 sub) (Bool.or (Kind.Term.fillable x2 sub) (Kind.Term.fillable x3 sub))))
+(Kind.Term.fillable (Kind.Term.ct5 ctid orig x0 x1 x2 x3 x4) 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) (Kind.Term.fillable x4 sub)))))
+(Kind.Term.fillable (Kind.Term.ct6 ctid orig x0 x1 x2 x3 x4 x5) 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) (Kind.Term.fillable x5 sub))))))
+(Kind.Term.fillable (Kind.Term.ct7 fnid orig args) sub) = (Kind.Term.fillable args sub)
+(Kind.Term.fillable (Kind.Term.ct8 fnid orig args) sub) = (Kind.Term.fillable args sub)
+(Kind.Term.fillable (Kind.Term.fn0 fnid orig) sub) = (Bool.false)
+(Kind.Term.fillable (Kind.Term.fn1 fnid orig x0) sub) = (Kind.Term.fillable x0 sub)
+(Kind.Term.fillable (Kind.Term.fn2 fnid orig x0 x1) sub) = (Bool.or (Kind.Term.fillable x0 sub) (Kind.Term.fillable x1 sub))
+(Kind.Term.fillable (Kind.Term.fn3 fnid orig x0 x1 x2) sub) = (Bool.or (Kind.Term.fillable x0 sub) (Bool.or (Kind.Term.fillable x1 sub) (Kind.Term.fillable x2 sub)))
+(Kind.Term.fillable (Kind.Term.fn4 fnid orig x0 x1 x2 x3) sub) = (Bool.or (Kind.Term.fillable x0 sub) (Bool.or (Kind.Term.fillable x1 sub) (Bool.or (Kind.Term.fillable x2 sub) (Kind.Term.fillable x3 sub))))
+(Kind.Term.fillable (Kind.Term.fn5 fnid orig x0 x1 x2 x3 x4) 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) (Kind.Term.fillable x4 sub)))))
+(Kind.Term.fillable (Kind.Term.fn6 fnid orig x0 x1 x2 x3 x4 x5) 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) (Kind.Term.fillable x5 sub))))))
+(Kind.Term.fillable (Kind.Term.fn7 fnid orig args) sub) = (Kind.Term.fillable args sub)
+(Kind.Term.fillable (Kind.Term.fn8 fnid orig args) sub) = (Kind.Term.fillable args sub)
+(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)
+
+// U60.equal (a: U60) (b: U60) : (Bool)
+(U60.equal a b) = (U60.to_bool (== a b))
+
+// U60.to_bool (n: U60) : (Bool)
+(U60.to_bool 0) = (Bool.false)
+(U60.to_bool n) = (Bool.true)
+
+// 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.Operator.equal (left: (Kind.Operator)) (right: (Kind.Operator)) : (Bool)
+(Kind.Operator.equal (Kind.Operator.and) (Kind.Operator.and)) = (Bool.true)
+(Kind.Operator.equal (Kind.Operator.sub) (Kind.Operator.sub)) = (Bool.true)
+(Kind.Operator.equal (Kind.Operator.mul) (Kind.Operator.mul)) = (Bool.true)
+(Kind.Operator.equal (Kind.Operator.div) (Kind.Operator.div)) = (Bool.true)
+(Kind.Operator.equal (Kind.Operator.mod) (Kind.Operator.mod)) = (Bool.true)
+(Kind.Operator.equal (Kind.Operator.and) (Kind.Operator.and)) = (Bool.true)
+(Kind.Operator.equal (Kind.Operator.or) (Kind.Operator.or)) = (Bool.true)
+(Kind.Operator.equal (Kind.Operator.xor) (Kind.Operator.xor)) = (Bool.true)
+(Kind.Operator.equal (Kind.Operator.shl) (Kind.Operator.shl)) = (Bool.true)
+(Kind.Operator.equal (Kind.Operator.shr) (Kind.Operator.shr)) = (Bool.true)
+(Kind.Operator.equal (Kind.Operator.ltn) (Kind.Operator.ltn)) = (Bool.true)
+(Kind.Operator.equal (Kind.Operator.lte) (Kind.Operator.lte)) = (Bool.true)
+(Kind.Operator.equal (Kind.Operator.eql) (Kind.Operator.eql)) = (Bool.true)
+(Kind.Operator.equal (Kind.Operator.gte) (Kind.Operator.gte)) = (Bool.true)
+(Kind.Operator.equal (Kind.Operator.gtn) (Kind.Operator.gtn)) = (Bool.true)
+(Kind.Operator.equal (Kind.Operator.neq) (Kind.Operator.neq)) = (Bool.true)
+(Kind.Operator.equal a 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.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))))