diff --git a/src/checker.hvm b/src/checker.hvm
index 807df9d4..2e33a2cc 100644
--- a/src/checker.hvm
+++ b/src/checker.hvm
@@ -67,34 +67,6 @@ Main =
     ]))
   ])
 
-//(Api.output [
-  //(Result (Negate.) [(Checked [(Ct1 (List.) (Ct0 (Bool.))), (Ct0 (Bool.))] 2 (Unit)), (Checked [] 0 (Unit))]),
-  //(Result (And.) [(Checked [] 0 (Unit)), (Checked [] 0 (Unit)), (Checked [] 0 (Unit)), (Checked [] 0 (Unit))]),
-  //(Result (Nil.) []),
-  //(Result (Main.) [(Errored (TypeMismatch (Ct0 (Nat.)) (Ct0 (Bool.))))]),
-  //(Result (Cons.) []),
-  //(Result (Zero.) []),
-  //(Result (Nat.) []),
-  //(Result (List.) []),
-  //(Result (Succ.) []),
-  //(Result (Bool.) []),
-  //(Result (False.) []),
-  //(Result (Not.) [(Checked [] 0 (Unit)), (Checked [] 0 (Unit))]),
-  //(Result (True.) []),
-  //(Result (Tail.) [(Errored (TypeMismatch (Ct1 (List.) (Inp 1)) (Ct1 (List.) (Var 0))))])
-//])
-
-//(Api.output Nil) = Nil
-//(Api.output (Cons (Result fn checks) results)) =
-  //(Text [
-    
-  //])
-
-
-//(Api.output (Cons (Errored err) results)) = (Cons (Some err) (Api.errors results))
-//(Api.output (Cons other results)) = (Api.errors results)
-
-
 // Prelude
 // -------
 
@@ -914,168 +886,3 @@ Main =
 // User-Defined Functions
 // ----------------------
 ////INJECT////
-
-  Functions =
-    let fns = Nil
-    let fns = (Cons And. fns)
-    let fns = (Cons Nil. fns)
-    let fns = (Cons List. fns)
-    let fns = (Cons Succ. fns)
-    let fns = (Cons True. fns)
-    let fns = (Cons Nat. fns)
-    let fns = (Cons Not. fns)
-    let fns = (Cons Bool. fns)
-    let fns = (Cons Negate. fns)
-    let fns = (Cons Tail. fns)
-    let fns = (Cons Main. fns)
-    let fns = (Cons False. fns)
-    let fns = (Cons Cons. fns)
-    let fns = (Cons Zero. fns)
-    fns
-
-  // And
-  // ---
-
-    (NameOf And.) = "And"
-    (HashOf And.) = %And
-    (TypeOf And.) = (All (Ct0 Bool.) λa (All (Ct0 Bool.) λb (Ct0 Bool.)))
-    (Rule2 And. (Ct0 True.) (Ct0 True.)) = (Ct0 True.)
-    (Rule2 And. (Ct0 True.) (Ct0 False.)) = (Ct0 False.)
-    (Rule2 And. (Ct0 False.) (Ct0 True.)) = (Ct0 False.)
-    (Rule2 And. (Ct0 False.) (Ct0 False.)) = (Ct0 False.)
-    (Verify And.) =
-      (Cons (LHS (Ct0 True.) (LHS (Ct0 True.) (RHS (Rule2 And. (Ct0 True.) (Ct0 True.)))))
-      (Cons (LHS (Ct0 True.) (LHS (Ct0 False.) (RHS (Rule2 And. (Ct0 True.) (Ct0 False.)))))
-      (Cons (LHS (Ct0 False.) (LHS (Ct0 True.) (RHS (Rule2 And. (Ct0 False.) (Ct0 True.)))))
-      (Cons (LHS (Ct0 False.) (LHS (Ct0 False.) (RHS (Rule2 And. (Ct0 False.) (Ct0 False.)))))
-      Nil))))
-
-  // Nil
-  // ---
-
-    (NameOf Nil.) = "Nil"
-    (HashOf Nil.) = %Nil
-    (TypeOf Nil.) = (All Typ λa (Ct1 List. a))
-    (Verify Nil.) =
-      Nil
-
-  // List
-  // ----
-
-    (NameOf List.) = "List"
-    (HashOf List.) = %List
-    (TypeOf List.) = (All Typ λa Typ)
-    (Verify List.) =
-      Nil
-
-  // Succ
-  // ----
-
-    (NameOf Succ.) = "Succ"
-    (HashOf Succ.) = %Succ
-    (TypeOf Succ.) = (All (Ct0 Nat.) λpred (Ct0 Nat.))
-    (Verify Succ.) =
-      Nil
-
-  // True
-  // ----
-
-    (NameOf True.) = "True"
-    (HashOf True.) = %True
-    (TypeOf True.) = (Ct0 Bool.)
-    (Verify True.) =
-      Nil
-
-  // Nat
-  // ---
-
-    (NameOf Nat.) = "Nat"
-    (HashOf Nat.) = %Nat
-    (TypeOf Nat.) = Typ
-    (Verify Nat.) =
-      Nil
-
-  // Not
-  // ---
-
-    (NameOf Not.) = "Not"
-    (HashOf Not.) = %Not
-    (TypeOf Not.) = (All (Ct0 Bool.) λa (Ct0 Bool.))
-    (Rule1 Not. (Ct0 True.)) = (Ct0 False.)
-    (Rule1 Not. (Ct0 False.)) = (Ct0 True.)
-    (Verify Not.) =
-      (Cons (LHS (Ct0 True.) (RHS (Rule1 Not. (Ct0 True.))))
-      (Cons (LHS (Ct0 False.) (RHS (Rule1 Not. (Ct0 False.))))
-      Nil))
-
-  // Bool
-  // ----
-
-    (NameOf Bool.) = "Bool"
-    (HashOf Bool.) = %Bool
-    (TypeOf Bool.) = Typ
-    (Verify Bool.) =
-      Nil
-
-  // Negate
-  // ------
-
-    (NameOf Negate.) = "Negate"
-    (HashOf Negate.) = %Negate
-    (TypeOf Negate.) = (All (Ct1 List. (Ct0 Bool.)) λxs (Ct1 List. (Ct0 Bool.)))
-    (Rule1 Negate. (Ct3 Cons. (Ct0 Bool.) x xs)) = (Ct3 Cons. (Ct0 Bool.) (Fn1 Not. x) (Fn1 Negate. xs))
-    (Rule1 Negate. (Ct1 Nil. (Ct0 Bool.))) = (Ct1 Nil. (Ct0 Bool.))
-    (Verify Negate.) =
-      (Cons (LHS (Ct3 Cons. (Ct0 Bool.) (Inp 0) (Inp 1)) (RHS (Rule1 Negate. (Ct3 Cons. (Ct0 Bool.) (Var 0) (Var 1)))))
-      (Cons (LHS (Ct1 Nil. (Ct0 Bool.)) (RHS (Rule1 Negate. (Ct1 Nil. (Ct0 Bool.)))))
-      Nil))
-
-  // Tail
-  // ----
-
-    (NameOf Tail.) = "Tail"
-    (HashOf Tail.) = %Tail
-    (TypeOf Tail.) = (All Typ λa (All (Ct1 List. a) λxs (Ct1 List. a)))
-    (Rule2 Tail. a (Ct3 Cons. t x xs)) = xs
-    (Verify Tail.) =
-      (Cons (LHS (Inp 0) (LHS (Ct3 Cons. (Inp 1) (Inp 2) (Inp 3)) (RHS (Rule2 Tail. (Var 0) (Ct3 Cons. (Var 1) (Var 2) (Var 3))))))
-      Nil)
-
-  // Main
-  // ----
-
-    (NameOf Main.) = "Main"
-    (HashOf Main.) = %Main
-    (TypeOf Main.) = (Ct1 List. (Ct0 Bool.))
-    (Rule0 Main.) = (Fn2 Tail. (Ct0 Bool.) (Ct3 Cons. (Ct0 Bool.) (Ct0 Zero.) (Ct3 Cons. (Ct0 Bool.) (Ct0 False.) (Ct1 Nil. (Ct0 Bool.)))))
-    (Verify Main.) =
-      (Cons (RHS (Rule0 Main.))
-      Nil)
-
-  // False
-  // -----
-
-    (NameOf False.) = "False"
-    (HashOf False.) = %False
-    (TypeOf False.) = (Ct0 Bool.)
-    (Verify False.) =
-      Nil
-
-  // Cons
-  // ----
-
-    (NameOf Cons.) = "Cons"
-    (HashOf Cons.) = %Cons
-    (TypeOf Cons.) = (All Typ λa (All a λx (All (Ct1 List. a) λxs (Ct1 List. a))))
-    (Verify Cons.) =
-      Nil
-
-  // Zero
-  // ----
-
-    (NameOf Zero.) = "Zero"
-    (HashOf Zero.) = %Zero
-    (TypeOf Zero.) = (Ct0 Nat.)
-    (Verify Zero.) =
-      Nil
-