add some #[compile-scheme]

examples/list.quox

@@ -24,6 +24,7 @@ def elim : 0.(A : ★) → 0.(P : (n : ℕ) → Vec n A → ★) →
         }
     };
 
+#[compile-scheme "(lambda% (n xs) xs)"]
 def up : 0.(A : ★) → (n : ℕ) → Vec n A → Vec¹ n A =
   λ A n ⇒
     case n return n' ⇒ Vec n' A → Vec¹ n' A of {
@@ -63,6 +64,7 @@ def elim : 0.(A : ★) → 0.(P : List A → ★) →
     };
 
 -- [fixme] List A <: List¹ A should be automatic, imo
+#[compile-scheme "(lambda (xs) xs)"]
 def up : 0.(A : ★) → List A → List¹ A =
   λ A xs ⇒
   case xs return List¹ A of { (len, elems) ⇒

examples/nat.quox

@@ -4,6 +4,7 @@ load "either.quox";
 
 namespace nat {
 
+#[compile-scheme "(lambda (n) (cons n 'erased))"]
 def dup! : (n : ℕ) → [ω. Sing ℕ n] =
   λ n ⇒
   case n return n' ⇒ [ω. Sing ℕ n'] of {
@@ -16,6 +17,7 @@ def dup! : (n : ℕ) → [ω. Sing ℕ n] =
 def dup : ℕ → [ω.ℕ] =
   λ n ⇒ appω (Sing ℕ n) ℕ (sing.val ℕ n) (dup! n);
 
+#[compile-scheme "(lambda% (m n) (+ m n))"]
 def plus : ℕ → ℕ → ℕ =
   λ m n ⇒
   case m return ℕ of {
@@ -23,6 +25,7 @@ def plus : ℕ → ℕ → ℕ =
     succ _, 1.p ⇒ succ p
   };
 
+#[compile-scheme "(lambda% (m n) (* m n))"]
 def timesω : ℕ → ω.ℕ → ℕ =
   λ m n ⇒
   case m return ℕ of {
@@ -67,6 +70,7 @@ def0 not-succ-self : (m : ℕ) → Not (m ≡ succ m : ℕ) =
   }
 
 
+#[compile-scheme "(lambda% (m n) (if (= m n) Yes No))"]
 def eq? : DecEq ℕ =
   λ m ⇒
   caseω m