From 9dcf782e58cd42bcca56372a8d22ec0831f84b0d Mon Sep 17 00:00:00 2001
From: whatisRT <andre.knispel@gmx.de>
Date: Tue, 26 Dec 2023 14:33:52 +0100
Subject: [PATCH] Prepare for scott encodings

---
 mced/Base/Inference.mced                  | 11 ++++----
 mced/Base/ReduceMultiApp.mced             |  9 +++---
 mced/Bootstrap/Stage-1/List.mced          | 34 +++++++++++++----------
 mced/Bootstrap/Stage-1/View.mced          | 12 ++++++++
 mced/Bootstrap/Stage-2/Term.mced          |  4 +--
 mced/Bootstrap/Stage-3/Eval.mced          | 15 +++++-----
 mced/Bootstrap/Stage-3/ListExt.mced       | 29 +++++++++----------
 mced/Bootstrap/Stage-3/Quoters.mced       |  4 +--
 mced/Bootstrap/Stage-3/StringHelpers.mced | 15 +++++++---
 mced/Bootstrap/Stage-3/TermHelpers.mced   |  4 +--
 mced/Bootstrap/Stage-3/TermRec.mced       |  3 +-
 mced/Test/Bootstrap/Eval.mced             |  5 ++--
 mced/Test/COC/Conversion.mced             | 11 ++++----
 mced/Test/Datatypes/ConstrFunctor.mced    |  8 +++---
 mced/Test/ErrorMonad.mced                 |  4 +--
 mced/Test/LambdaCalcExample.mced          |  2 --
 mced/Test/SchemeCompiler/Test.mced        |  4 +--
 17 files changed, 99 insertions(+), 75 deletions(-)

diff --git a/mced/Base/Inference.mced b/mced/Base/Inference.mced
index 69ed3da..4091931 100644
--- a/mced/Base/Inference.mced
+++ b/mced/Base/Inference.mced
@@ -54,10 +54,9 @@ let isSolved (l : List App) : Bool :=
   isNil ?App (filter ?App (λ a : App. isUnknown $ appTerm a) l).
 
 let sequenceRecApp (recapp : List (Bool × Eval Term)) : Eval (List App) :=
-  sequenceEval ?App $
-    map ?(Bool × Eval Term) ?(Eval App)
-      (recursionProduct ?Bool ?(Eval Term) ?(Eval App) λ b : Bool. λ t : Eval Term.
-        mapEval ?Term ?App (mkApp b) t)
+  traverseEval ?(Bool × Eval Term) ?App
+    (recursionProduct ?Bool ?(Eval Term) ?(Eval App) λ b : Bool. λ t : Eval Term.
+      mapEval ?Term ?App (mkApp b) t)
     recapp.
 
 -- apply f to all applications in a term
@@ -172,8 +171,8 @@ let tryHNFEqn : UnsEqn -> Eval UnsEqn :=
     pureEval ?UnsEqn $ mkUnsEqn' eqnC t1 t2.
 
 -- partition equations into solved and unsolved
-let partitionSolved (ctx : Nat) (eqns : List UnsEqn) : List SEqn × List UnsEqn :=
-  eqns ?(List SEqn × List UnsEqn)
+let partitionSolved (ctx : Nat) : List UnsEqn -> List SEqn × List UnsEqn :=
+  recursionList' ?UnsEqn ?(List SEqn × List UnsEqn)
     (prodPair ?(List SEqn) ?(List UnsEqn) [SEqn|] [UnsEqn|])
     (λ eq : UnsEqn. λ rec : List SEqn × List UnsEqn.
       maybe ?SEqn ?(List SEqn × List UnsEqn)
diff --git a/mced/Base/ReduceMultiApp.mced b/mced/Base/ReduceMultiApp.mced
index ed91618..730415e 100644
--- a/mced/Base/ReduceMultiApp.mced
+++ b/mced/Base/ReduceMultiApp.mced
@@ -11,16 +11,17 @@ let reduceMultiApp : Term -> Term :=
       (λ t1 : Term. λ app1 : List App.
         ψ reduceAppL = map ?App ?App $ productMap2 ?Bool ?Term ?Term reduceMultiApp
                       : List App -> List App.
-        ψ t          = appLTerm (reduceMultiApp t1) (reduceAppL app1) : Term. matchTerm ?Term
+        ψ t1r        = reduceMultiApp t1 : Term.
+        ψ app1r      = reduceAppL app1 : List App.
+        ψ t          = appLTerm t1r app1r : Term. matchTerm ?Term
           (λ _ : Var. t)
           (λ _ : Sort. t)
           (λ _ : Binder. λ _ : String. λ _, _ : Term. t)
-          (λ t2 : Term. λ app2 : List App.
-            reduceMultiApp $ appLTerm t2 (reduceAppL $ app ?App app2 app1))
+          (λ t2 : Term. λ app2 : List App. appLTerm t2 (app ?App app2 app1r))
           (λ _ : Char. t)
           t
           (λ _ : Term. t)
-          t1)
+          t1r)
       charTerm
       unknownTerm
       (λ t : Term. unquoteTerm (reduceMultiApp t)).
diff --git a/mced/Bootstrap/Stage-1/List.mced b/mced/Bootstrap/Stage-1/List.mced
index 99bcc9e..3b1b2ec 100644
--- a/mced/Bootstrap/Stage-1/List.mced
+++ b/mced/Bootstrap/Stage-1/List.mced
@@ -28,14 +28,20 @@ let recursionList' := Λ A : * Λ X : * λ rn : X λ rc : Π _ : A Π _ : X X λ
   [[<l X> rn] rc]
   : ∀ A : * ∀ X : * Π rn : X Π rc : Π _ : A Π _ : X X Π l : [List A] X.
 
-let length := Λ X : * λ l : [List X]
-  [[<l Nat> zero] λ x : X λ n : Nat [suc n]]
+let matchList' := Λ A : * Λ X : * λ rn : X λ rc : Π _ : A Π _ : [List A] X
+  [[<<recursionList A> X> rn] λ a : A λ as : [List A] λ _ : X [[rc a] as]]
+  : ∀ A : * ∀ X : * Π _ : X Π _ : Π _ : A Π _ : [List A] X Π _ : [List A] X.
+
+--------------------------------------------------------------------------------
+
+let length := Λ X : *
+  [[<<recursionList' X> Nat> zero] λ x : X λ n : Nat [suc n]]
   : ∀ X : * Π _ : [List X] Nat.
 
 let nilLength := Λ X : * β zero zero : ∀ X : * = zero [<length X> <nil X>].
 
-let isNil := Λ X : * λ l : [List X]
-  [[<l Bool> true] λ _ : X λ _ : Bool false]
+let isNil := Λ X : *
+  [[<<matchList' X> Bool> true] λ _ : X λ _ : [List X] false]
   : ∀ X : * Π _ : [List X] Bool.
 
 let listEq := Λ X : * λ eqX : Π _ : X Π _ : X Bool
@@ -47,27 +53,27 @@ let listEq := Λ X : * λ eqX : Π _ : X Π _ : X Bool
 let pureList := Λ X : * λ x : X [[<cons X> x] <nil X>] : ∀ X : * Π _ : X [List X].
 
 let app := Λ X : * λ l1 : [List X] λ l2 : [List X]
-  [[<l1 [List X]> l2] λ x : X λ rec : [List X] [[<cons X> x] rec]]
+  [[[<<recursionList' X> [List X]> l2] λ x : X λ rec : [List X] [[<cons X> x] rec]] l1]
   : ∀ X : * Π _ : [List X] Π _ : [List X] [List X].
 
 let snoc := Λ X : * λ x : X λ xs : [List X] [[<app X> xs] [<pureList X> x]]
   : ∀ X : * Π _ : X Π _ : [List X] [List X].
 
-let filter := Λ X : * λ f : Π _ : X Bool λ l : [List X]
-  [[<l [List X]> <nil X>]
+let filter := Λ X : * λ f : Π _ : X Bool
+  [[<<recursionList' X> [List X]> <nil X>]
     λ x : X λ rec : [List X] [[[<ifthenelse [List X]> [f x]] [[<cons X> x] rec]] rec]]
   : ∀ X : * Π f : Π _ : X Bool Π _ : [List X] [List X].
 
-let foldl := Λ A : * Λ B : * λ f : (Π _ : B Π _ : A B) λ l : [List A]
-  [[<l Π _ : B B>
+let foldl := Λ A : * Λ B : * λ f : (Π _ : B Π _ : A B)
+  [[<<recursionList' A> Π _ : B B>
   λ b : B b]
   λ a : A λ rec : Π _ : B B λ b : B [[f [rec b]] a]].
 
 let foldr := Λ A : * Λ B : * λ f : (Π _ : A Π _ : B B) λ l : [List A] λ b : B
-  [[<l B> b] λ a : A λ rec : B [[f a] rec]].
+  [[[<<recursionList' A> B> b] λ a : A λ rec : B [[f a] rec]] l].
 
-let reverseAcc := Λ X : * λ l : [List X]
-  [[<l Π _ : [List X] [List X]>
+let reverseAcc := Λ X : *
+  [[<<recursionList' X> Π _ : [List X] [List X]>
     λ acc : [List X] acc]
     λ x : X λ rec : Π _ : [List X] [List X] λ acc : [List X] [rec [[<cons X> x] acc]]].
 
@@ -79,8 +85,8 @@ let scanl := Λ A : * Λ B : * λ f : (Π _ : B Π _ : A B) λ b : B
   [<pureList B> b]]
   λ a : A λ as : [List A] λ rec : [List B] [[<cons B> [[[<<foldl A> B> f] [[<cons A> a] as]] b]] rec]].
 
-let map := Λ X : * Λ Y : * λ f : Π _ : X Y λ l : [List X]
-  [[<l [List Y]> <nil Y>] λ x : X λ rec : [List Y] [[<cons Y> [f x]] rec]].
+let map := Λ X : * Λ Y : * λ f : Π _ : X Y
+  [[<<recursionList' X> [List Y]> <nil Y>] λ x : X λ rec : [List Y] [[<cons Y> [f x]] rec]].
 
 let intersperse :=
   Λ X : * λ x : X λ l : [List X] [[[<<recursionList X> [List X]> <nil X>]
diff --git a/mced/Bootstrap/Stage-1/View.mced b/mced/Bootstrap/Stage-1/View.mced
index 55e32df..7584a9b 100644
--- a/mced/Bootstrap/Stage-1/View.mced
+++ b/mced/Bootstrap/Stage-1/View.mced
@@ -6,9 +6,17 @@ let beta := Λ X : * λ x : X β x x.
 let idTop := λ x : * x.
 let Top := = idTop idTop.
 
+let beta' := Λ X : * λ x : X β idTop x.
+
 let intrTop := β idTop idTop : Top.
 let toTop := Λ T : * λ t : T β idTop t : ∀ T : * Π _ : T Top.
 
+let ycomb := Λ T : * λ t : (Π _ : T T) β idTop [λ x : * [t [x x]] λ x : * [t [x x]]]
+  : ∀ T : * Π _ : (Π _ : T T) Top.
+
+let ycombBeta := Λ T : * λ f : (Π _ : T T) β [ycomb f] [ycomb f]
+  : ∀ T : * Π f : (Π _ : T T) (= [ycomb f] [f [ycomb f]]).
+
 let conv := Λ S : * Λ T : * Λ s : S λ t : T Λ eq : (= s t) φ eq s t.
 
 let View := λ T : * λ t : Top ι x : T (= x t) : Π T : * Π _ : Top *.
@@ -36,6 +44,10 @@ let extView := Λ S : * Λ T : * λ t : Top Λ v : Π x : S [[View T] β idTop [
 let Cast := λ S : * λ T : * [[View Π _ : S T] intrTop]
   : Π S : * Π T : * *.
 
+let extCast := Λ S : * Λ T : * Λ v : Π x : S [[View T] [<beta' S> x]]
+  <[<<extView S> T> intrTop] v>
+  : ∀ S : * ∀ T : * ∀ _ : (Π x : S [[View T] [<beta' S> x]]) [[Cast S] T].
+
 let intrCast := Λ S : * Λ T : * Λ t : (Π _ : S T) Λ t' : (Π x : S = [t x] x)
  <[<<extView S> T> intrTop] (λ x : S <<[<intrView T> β idTop x] [t x]> [t' x]>)>
   : ∀ S : * ∀ T : * ∀ t : (Π _ : S T) ∀ _ : (Π x : S = [t x] x) [[Cast S] T].
diff --git a/mced/Bootstrap/Stage-2/Term.mced b/mced/Bootstrap/Stage-2/Term.mced
index a6847e2..a806edd 100644
--- a/mced/Bootstrap/Stage-2/Term.mced
+++ b/mced/Bootstrap/Stage-2/Term.mced
@@ -234,9 +234,9 @@ let multiTermRest := <<pr2 Term> [List [[Product Term] InfixData]]>
 --     : Π _ : MultiTerm Term.
 
 let multiTermToTermRight := λ m : MultiTerm
-  [[[<<recursionList [[Product Term] InfixData]> Term>
+  [[[<<matchList' [[Product Term] InfixData]> Term>
     [multiTermSingle m]]
-    λ h : [[Product Term] InfixData] λ t : [List [[Product Term] InfixData]] λ _ : Term
+    λ h : [[Product Term] InfixData] λ t : [List [[Product Term] InfixData]]
       [[appToTerm
         [[[<<foldr [[Product Term] InfixData]> [[Product Term] InfixData]>
           λ x : [[Product Term] InfixData] λ acc : [[Product Term] InfixData]
diff --git a/mced/Bootstrap/Stage-3/Eval.mced b/mced/Bootstrap/Stage-3/Eval.mced
index 03a2015..c114d4c 100644
--- a/mced/Bootstrap/Stage-3/Eval.mced
+++ b/mced/Bootstrap/Stage-3/Eval.mced
@@ -166,8 +166,8 @@ b-let mapEval [T, T' : *] (f : T -> T') (t : Eval T) : Eval T' :=
   bindEval ?T ?T' t (λ x : T. pureEval ?T' (f x)).
 b-let seqEval [T, T' : *] (t : Eval T) (t' : Eval T') : Eval T' :=
   bindEval ?T ?T' t (λ _ : T. t').
-b-let sequenceEval [T : *] (l : List (Eval T)) : Eval (List T) :=
-  l ?(Eval (List T))
+b-let sequenceEval [T : *] : List (Eval T) -> Eval (List T) :=
+  recursionList' ?(Eval T) ?(Eval (List T))
     (pureEval ?(List T) (nil ?T))
     (λ x : Eval T. λ rec : Eval (List T). bindEval ?T ?(List T) x
       λ x' : T. mapEval ?(List T) ?(List T) (cons ?T x') rec).
@@ -229,7 +229,7 @@ b-let annLet (n : String) (t, T : Term) : Eval Unit :=
 b-let setMEnv (eval : Term) (NT, ns : String) : Eval Unit :=
   liftMtoEval ?Unit (primSetEval (TermToInitTerm eval) NT ns).
 b-let shellCmd (cmd : String) (args : List String) : Eval String :=
-  liftMtoEval ?String (primShellCmd cmd args).
+  liftMtoEval ?String (primShellCmd cmd (listStringToStringList args)).
 b-let checkTerm (T : *) (t : Term) : Eval T :=
   liftMtoEval ?T (primCheckTerm T (TermToInitTerm t)).
 b-let parse (nt : String) (T : *) (text : String) : Eval (Product T String) :=
@@ -257,10 +257,11 @@ b-let writeFile (fName, s : String) : Eval Unit :=
   liftMtoEval ?Unit (primWriteFile fName s).
 
 b-let commandLine : Eval (List String) :=
-  liftMtoEval ?(List String) primCommandLine.
+  mapEval ?init$stringList ?(List String) stringListToListString
+    (liftMtoEval ?init$stringList primCommandLine).
 
 b-let setDebug (opts : List String) : Eval Unit :=
-  liftMtoEval ?Unit (primSetDebug opts).
+  liftMtoEval ?Unit (primSetDebug (listStringToStringList opts)).
 
 b-let printLineEval (s : String) : Eval Unit := printEval φ"${s}\n".
 
@@ -318,9 +319,9 @@ b-let letInfoToNewStmt (i : LetInfo) : Eval Unit :=
 b-let ElabLet : * := LetInfo -> Eval LetInfo.
 
 b-let runEvalLets' : List ElabLet -> ElabLet :=
-  recursionList ?ElabLet ?ElabLet
+  recursionList' ?ElabLet ?ElabLet
     (pureEval ?LetInfo)
-    (λ el : ElabLet. λ _ : List ElabLet. λ rec : ElabLet.
+    (λ el : ElabLet. λ rec : ElabLet.
       λ i : LetInfo. bindEval ?LetInfo ?LetInfo (el i) rec).
 
 b-let runEvalLets (els : List ElabLet) (i : LetInfo) : Eval Unit :=
diff --git a/mced/Bootstrap/Stage-3/ListExt.mced b/mced/Bootstrap/Stage-3/ListExt.mced
index 8310c42..ea5ee04 100644
--- a/mced/Bootstrap/Stage-3/ListExt.mced
+++ b/mced/Bootstrap/Stage-3/ListExt.mced
@@ -9,17 +9,17 @@ b-let showList [X : *] (showX : X -> String) (l : List X) : String :=
   φ"[${stringConcat (intersperse ?String ", " (map ?X ?String showX l))}]".
 
 b-let lookupDefault [A : *] (n : Nat) (d : A) (l : List A) : A :=
-  l ?(Nat -> A)
+  recursionList' ?A ?(Nat -> A)
     (λ _ : Nat. d)
     (λ a : A. λ rec : Nat -> A.
       recursionNat ?A a (λ k : Nat. λ _ : A. rec k))
-    n.
+    l n.
 
-b-let head [A : *] (l : List A) : Maybe A :=
-  l ?(Maybe A) (nothing ?A) (λ a : A. λ _ : Maybe A. just ?A a).
+b-let head [A : *] : List A -> Maybe A :=
+  matchList' ?A ?(Maybe A) (nothing ?A) (λ a : A. λ _  : List A. just ?A a).
 
-b-let tail [A : *] (l : List A) : List A :=
-  recursionList ?A ?(List A) [A|] (λ a : A. λ l' : List A. λ _ : List A. l') l.
+b-let tail [A : *] : List A -> List A :=
+  matchList' ?A ?(List A) [A|]          (λ _ : A. λ as : List A. as).
 
 b-let findMaybe [A : *] (P : A -> Bool) (l : List A) : Maybe A :=
   head ?A (filter ?A P l).
@@ -34,8 +34,8 @@ b-let maybeToList [A : *] : Maybe A -> List A :=
   maybe ?A ?(List A) [A|] (λ a : A. [A|a]).
 
 b-let mapHead [A : *] (f : Maybe A -> Maybe A) : List A -> List A :=
-  recursionList ?A ?(List A) (maybeToList ?A (f (nothing ?A)))
-    (λ a : A. λ as, _ : List A. app ?A (maybeToList ?A (f (just ?A a))) as).
+  matchList' ?A ?(List A) (maybeToList ?A (f (nothing ?A)))
+    (λ a : A. λ as : List A. app ?A (maybeToList ?A (f (just ?A a))) as).
 
 b-let initsNonEmpty [A : *] (l : List A) : List (Product A (List A)) :=
   recursionList ?A ?(List (Product A (List A)))
@@ -60,13 +60,14 @@ b-let countToZeroExc (n : Nat) :=
     n.
 
 b-let zipWith [A, B, C : *] (f : A -> B -> C) (l : List A) (l' : List B) : List C :=
-  l ?(List B -> List C)
+  recursionList' ?A ?(List B -> List C)
     (λ _ : List B. [C|])
     (λ a : A. λ rec : List B -> List C.
-      recursionList ?B ?(List C) [C|] (λ b : B. λ bs : List B. λ _ : List C. cons ?C (f a b) (rec bs)))
-    l'.
+      matchList' ?B ?(List C) [C|] (λ b : B. λ bs : List B. cons ?C (f a b) (rec bs)))
+    l l'.
 
-b-let zip [A, B : *] (l : List A) (l' : List B) : List (Product A B) := zipWith ?A ?B ?(Product A B) (prodPair ?A ?B) l l'.
+b-let zip [A, B : *] (l : List A) (l' : List B) : List (Product A B) :=
+  zipWith ?A ?B ?(Product A B) (prodPair ?A ?B) l l'.
 
 b-let zipWith3 [A, B, C, D : *] (f : A -> B -> C -> D) (l : List A) (l' : List B) (l'' : List C) : List D :=
   zipWith ?A ?(Product B C) ?D (λ a : A. λ bc : Product B C. f a (pr1 ?B ?C bc) (pr2 ?B ?C bc)) l (zip ?B ?C l' l'').
@@ -80,8 +81,8 @@ b-let zipWith4 [A, B, C, D, E : *] (f : A -> B -> C -> D -> E)
     (λ a : A. λ bcd : TripleProduct B C D.
       f a (pr31 ?B ?C ?D bcd) (pr32 ?B ?C ?D bcd) (pr33 ?B ?C ?D bcd)) l (zip3 ?B ?C ?D l' l'' l''').
 
-b-let concat [A : *] (l : List (List A)) : List A :=
-  l ?(List A) [A|] (λ l' : List A. λ rec : List A. app ?A l' rec).
+b-let concat [A : *] : List (List A) -> List A :=
+  recursionList' ?(List A) ?(List A) [A|] (λ l' : List A. λ rec : List A. app ?A l' rec).
 
 b-let drop [A : *] (n : Nat) (l : List A) : List A :=
   n ?(List A) l (tail ?A).
diff --git a/mced/Bootstrap/Stage-3/Quoters.mced b/mced/Bootstrap/Stage-3/Quoters.mced
index add32aa..3d0f845 100644
--- a/mced/Bootstrap/Stage-3/Quoters.mced
+++ b/mced/Bootstrap/Stage-3/Quoters.mced
@@ -7,5 +7,5 @@ b-let quoteProduct [A, B : *] (quotedA, quotedB : Term) (quoteA : A -> Term) (qu
   λ x : Product A B. θ{prodPair ?γ{quotedA} ?γ{quotedB} γ{quoteA (pr1 ?A ?B x)} γ{quoteB (pr2 ?A ?B x)}}.
 
 b-let quoteList [X : *] (quotedX : Term) (quoteX : X -> Term) : List X -> Term :=
-  recursionList ?X ?Term θ{nil ?γ{quotedX}}
-    (λ x : X. λ _ : List X. λ rec : Term. θ{cons ?γ{quotedX} γ{quoteX x} γ{rec}}).
+  recursionList' ?X ?Term θ{nil ?γ{quotedX}}
+    (λ x : X. λ rec : Term. θ{cons ?γ{quotedX} γ{quoteX x} γ{rec}}).
diff --git a/mced/Bootstrap/Stage-3/StringHelpers.mced b/mced/Bootstrap/Stage-3/StringHelpers.mced
index e0d97b4..6b10aaf 100644
--- a/mced/Bootstrap/Stage-3/StringHelpers.mced
+++ b/mced/Bootstrap/Stage-3/StringHelpers.mced
@@ -5,16 +5,23 @@
 b-let stringToList (s : String) : List Char :=
   s ?(List Char) (λ c : Char. λ rec : List Char. cons ?Char c rec) (nil ?Char).
 
-b-let stringFromList (s : List Char) : String :=
-  s ?String stringNil stringCons.
+b-let stringFromList : List Char -> String :=
+  recursionList' ?Char ?String stringNil stringCons.
 
 b-let stringApp (s, s' : String) : String :=
   s ?String stringCons s'.
 
-b-let stringConcat (l : List String) : String :=
-  l ?String stringNil stringApp.
+b-let stringConcat : List String -> String :=
+  recursionList' ?String ?String stringNil stringApp.
 
 -- Equality
 
 b-let stringEq (s, s' : String) : Bool :=
   listEq ?Char charEq (stringToList s) (stringToList s').
+
+b-let listStringToStringList : List String -> init$stringList :=
+  recursionList' ?String ?init$stringList
+    stringListNil stringListCons.
+
+b-let stringListToListString (s : init$stringList) : List String :=
+  s ?(List String) (nil ?String) (cons ?String).
diff --git a/mced/Bootstrap/Stage-3/TermHelpers.mced b/mced/Bootstrap/Stage-3/TermHelpers.mced
index 04ad615..33a856c 100644
--- a/mced/Bootstrap/Stage-3/TermHelpers.mced
+++ b/mced/Bootstrap/Stage-3/TermHelpers.mced
@@ -19,9 +19,9 @@ let indexToIndex' (i : DBIndex) : DBIndex' :=
 
 let digitListToIndex' (l : List Dec) : DBIndex' := foldl ?Dec ?DBIndex' consDecToIndex' l init$index'$.
 let digitListToIndex : List Dec -> DBIndex :=
-  recursionList ?Dec ?DBIndex
+  matchList' ?Dec ?DBIndex
     (init$index$0_index'_ init$index'$)
-    (λ d : Dec. λ ds : List Dec. λ _ : DBIndex. consDecToIndex (digitListToIndex' ds) d).
+    (λ d : Dec. λ ds : List Dec. consDecToIndex (digitListToIndex' ds) d).
 
 let natToIndex (n : Nat) : DBIndex := digitListToIndex $ natToDecList n.
 let natToVar (n : Nat) : Term := varTerm $ init$var$_index_ $ natToIndex n.
diff --git a/mced/Bootstrap/Stage-3/TermRec.mced b/mced/Bootstrap/Stage-3/TermRec.mced
index 7fec7df..4b9d7ec 100644
--- a/mced/Bootstrap/Stage-3/TermRec.mced
+++ b/mced/Bootstrap/Stage-3/TermRec.mced
@@ -10,8 +10,7 @@ b-let mapAppList [X, Y : *] (f : X -> Y) (l : List (Product Bool X)) : List (Pro
 
 b-let distList [X, Y, Z : *]
   : List (TripleProduct X Y Z) -> Product (List (Product X Y)) (List (Product X Z)) :=
-  λ l : List (TripleProduct X Y Z).
-  l ?(Product (List (Product X Y)) (List (Product X Z)))
+  recursionList' ?(TripleProduct X Y Z) ?(Product (List (Product X Y)) (List (Product X Z)))
     (prodPair ?(List (Product X Y)) ?(List (Product X Z)) (nil ?(Product X Y)) (nil ?(Product X Z)))
     (recursionTripleProduct ?X ?Y ?Z
       ?(Product (List (Product X Y)) (List (Product X Z))
diff --git a/mced/Test/Bootstrap/Eval.mced b/mced/Test/Bootstrap/Eval.mced
index b0643b6..3215dca 100644
--- a/mced/Test/Bootstrap/Eval.mced
+++ b/mced/Test/Bootstrap/Eval.mced
@@ -333,10 +333,9 @@ elet letInfoToNewStmt (i : LetInfo) : Eval Unit :=
 
 let ElabLet : * := LetInfo -> Eval LetInfo.
 
-elet runEvalLets' : List ElabLet -> ElabLet := recursionList ?_ ?_
+elet runEvalLets' : List ElabLet -> ElabLet := recursionList' ?_ ?_
   (pureEval ?LetInfo)
-  (λ el : ElabLet. λ _ : List ElabLet. λ rec : ElabLet.
-    λ i : LetInfo. el i >>= rec).
+  (λ el : ElabLet. λ rec : ElabLet. λ i : LetInfo. el i >>= rec).
 
 elet runEvalLets (els : List ElabLet) (i : LetInfo) : Eval Unit :=
   runEvalLets' els i >>= letInfoToNewStmt.
diff --git a/mced/Test/COC/Conversion.mced b/mced/Test/COC/Conversion.mced
index 19ac209..46bbb00 100644
--- a/mced/Test/COC/Conversion.mced
+++ b/mced/Test/COC/Conversion.mced
@@ -6,7 +6,7 @@ module COC:Conversion.
 
 Given MCTerm MCSVar MCAst MCSq MCLambda MCPi MCApp natToVar indexToNat init$index.
 Given MCVar MCSort Binder String stringCons stringNil stringEq Char.
-Given List cons nil reverse Product Bool true false ifthenelse pr1 pr2.
+Given List cons nil recursionList' reverse Product Bool true false ifthenelse pr1 pr2.
 Given TripleProduct mkTripleProduct pr31 pr32 pr33.
 Given LetInfo letInfoName letInfoTerm letInfoType.
 Given Maybe just nothing maybe bindMaybe mapMaybe.
@@ -15,8 +15,8 @@ importModule DatatypesTest:Nat.
 importModule DatatypesTest:NatConversions.
 importModule COC:Theory.
 
-let findMaybe [A : *] (pred : A -> Bool) (l : List A) : Maybe Nat :=
-  l ?(Maybe Nat)
+let findMaybe [A : *] (pred : A -> Bool) : List A -> Maybe Nat :=
+  recursionList' ?A ?(Maybe Nat)
     (nothing ?Nat)
     (λ a : A. λ rec : Maybe Nat. ifthenelse ?(Maybe Nat) (pred a) (just ?Nat zero) (mapMaybe ?Nat ?Nat succ rec)).
 
@@ -36,14 +36,15 @@ let toCOCTerm (t : MCTerm) : Maybe Term :=
             (just ?Term (Pi x x'))
             (nothing ?Term)) (t' (cons ?String n l))) (t l))
     (λ t : List String -> Maybe Term. λ app : List (Product Bool (List String -> Maybe Term)). λ l : List String.
-      (reverse ?(Product Bool (List String -> Maybe Term)) app) ?(Maybe Term)
+      recursionList' ?(Product Bool (List String -> Maybe Term)) ?(Maybe Term)
         (t l)
         (λ a : Product Bool (List String -> Maybe Term). λ rec : Maybe Term.
           maybe ?Term ?(Maybe Term) (nothing ?Term)
             (λ x : Term. ifthenelse ?(Maybe Term) (pr1 ?Bool ?(List String -> Maybe Term) a)
               (nothing ?Term)
               (maybe ?Term ?(Maybe Term) (nothing ?Term)
-                (λ x' : Term. just ?Term (App x' x)) rec)) (pr2 ?Bool ?(List String -> Maybe Term) a l)))
+                (λ x' : Term. just ?Term (App x' x)) rec)) (pr2 ?Bool ?(List String -> Maybe Term) a l))
+        (reverse ?(Product Bool (List String -> Maybe Term)) app))
     (λ _ : Char. λ _ : List String. nothing ?Term)
     (λ _ : List String. nothing ?Term)
     (λ _ : List String -> Maybe Term. λ _ : List String. nothing ?Term) -- nothing on unquote
diff --git a/mced/Test/Datatypes/ConstrFunctor.mced b/mced/Test/Datatypes/ConstrFunctor.mced
index de87785..556f03f 100644
--- a/mced/Test/Datatypes/ConstrFunctor.mced
+++ b/mced/Test/Datatypes/ConstrFunctor.mced
@@ -88,9 +88,9 @@ let ConstrFunctorF (name : String) (f : ConstrFunctorData) : Term :=
   ConstrFunctorF' name $ FoldConstrFunctorData f.
 
 let ApplyConstrFunctorData (f : ConstrFunctorData) (t : Term) : Term :=
-  recursionList ?CFParam ?Term
+  recursionList' ?CFParam ?Term
     t
-    (λ p : CFParam. λ ps : List CFParam. λ rec : Term.
+    (λ p : CFParam. λ rec : Term.
       piTerm (cfParamName p) (ApplyConstrFunctor t $ cfParamFunctor p) rec)
     f.
 
@@ -113,8 +113,8 @@ let ConstrFunctorFunctor (name : String) (f : ConstrFunctorData) : Term :=
 
 -- Turn a list of constructors into a functor
 let ConstrsFunctorF' (name : String) (constrs : List ConstrFunctorData) : Term :=
-  recursionList ?ConstrFunctorData ?Term θ{constF Void}
-    (λ f : ConstrFunctorData. λ fs : List ConstrFunctorData. λ rec : Term. θ{FunctorSumF γ{ConstrFunctorF name f} γ{rec}})
+  recursionList' ?ConstrFunctorData ?Term θ{constF Void}
+    (λ f : ConstrFunctorData. λ rec : Term. θ{FunctorSumF γ{ConstrFunctorF name f} γ{rec}})
     constrs.
 
 let ConstrsFunctorFunctor' (name : String) (constrs : List ConstrFunctorData) : Term :=
diff --git a/mced/Test/ErrorMonad.mced b/mced/Test/ErrorMonad.mced
index cc3a557..ab1c99b 100644
--- a/mced/Test/ErrorMonad.mced
+++ b/mced/Test/ErrorMonad.mced
@@ -20,6 +20,6 @@ elet liftError2 [A, B, C : *] (f : A -> B -> C) (a : Error A) (b : Error B) : Er
   bindError ?_ ?_ (λ a' : A. mapError ?_ ?_ (f a') b) a.
 
 elet traverseErrorList [X, Y : *] (f : X -> Error Y) : List X -> Error (List Y) :=
-  recursionList ?_ ?_
+  recursionList' ?_ ?_
     (pureError ?_ (nil ?Y))
-    (λ x : X. λ xs : List X. λ rec : Error (List Y). liftError2 ?_ ?_ ?_ (cons ?Y) (f x) rec).
+    (λ x : X. λ rec : Error (List Y). liftError2 ?_ ?_ ?_ (cons ?Y) (f x) rec).
diff --git a/mced/Test/LambdaCalcExample.mced b/mced/Test/LambdaCalcExample.mced
index bc226ac..2c74163 100644
--- a/mced/Test/LambdaCalcExample.mced
+++ b/mced/Test/LambdaCalcExample.mced
@@ -1,5 +1,3 @@
-λ-let ycomb := λ t. [λ x. [t [x x]] λ x. [t [x x]]].
-
 λ-let cZero := λ z. λ f. z.
 λ-let cSuc := λ n. λ z. λ f. [f [[n z] f]].
 
diff --git a/mced/Test/SchemeCompiler/Test.mced b/mced/Test/SchemeCompiler/Test.mced
index 1b3fb54..3888161 100644
--- a/mced/Test/SchemeCompiler/Test.mced
+++ b/mced/Test/SchemeCompiler/Test.mced
@@ -36,9 +36,9 @@ let schemePrintNat (n : SchemeNat) : SchemeFFI Unit :=
 let printSquare (n : Nat) : SchemeFFI Unit := schemePrintNat (evalNat $ square n).
 
 let printSquares (l : List Nat) : SchemeFFI Unit :=
-  recursionList ?Nat ?(SchemeFFI Unit)
+  recursionList' ?Nat ?(SchemeFFI Unit)
     (pureScheme ?Unit tt)
-    (λ n : Nat. λ _ : List Nat. λ x : SchemeFFI Unit.
+    (λ n : Nat. λ x : SchemeFFI Unit.
       seqScheme ?Unit ?Unit (printSquare n) x)
     l.