From b7e1f37b5b7f7309f76d1cdb9ebc461c21a286f0 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Fri, 3 Nov 2023 17:42:44 +0100
Subject: [PATCH] add some #[compile-scheme]

---
 examples/list.quox | 2 ++
 examples/nat.quox  | 4 ++++
 2 files changed, 6 insertions(+)

diff --git a/examples/list.quox b/examples/list.quox
index cb6ac1e..ac45ba4 100644
--- a/examples/list.quox
+++ b/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) ⇒
diff --git a/examples/nat.quox b/examples/nat.quox
index 17715d4..e194206 100644
--- a/examples/nat.quox
+++ b/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