From d115672d49527e4112619153f11755da76a25d8b Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Fri, 10 Nov 2023 15:07:19 +0100
Subject: [PATCH] example stuff

---
 examples/hello.quox |  2 --
 examples/misc.quox  |  5 +++++
 examples/nat.quox   | 52 ++++++++++++++++++++++++++++++++++++---------
 examples/qty.quox   | 10 ++++++---
 4 files changed, 54 insertions(+), 15 deletions(-)

diff --git a/examples/hello.quox b/examples/hello.quox
index e1f2052..3b7122e 100644
--- a/examples/hello.quox
+++ b/examples/hello.quox
@@ -3,8 +3,6 @@ def0 Unit : ★ = {tt}
 def drop-unit : 0.(A : ★) → Unit → A → A =
   λ A u x ⇒ case u return A of {'tt ⇒ x}
 
--- postulate0 IOState : ★
-
 def0 IO : ★ → ★ = λ A ⇒ IOState → A × IOState
 
 def bind : 0.(A B : ★) → IO A → (A → IO B) → IO B =
diff --git a/examples/misc.quox b/examples/misc.quox
index bf24d39..8afbde9 100644
--- a/examples/misc.quox
+++ b/examples/misc.quox
@@ -14,6 +14,11 @@ def0 cong :
     (x y : A) → (xy : x ≡ y : A) → Eq (𝑖 ⇒ P (xy @𝑖)) (p x) (p y) =
   λ A P p x y xy ⇒ δ 𝑖 ⇒ p (xy @𝑖)
 
+def0 cong' :
+    (A B : ★) → (f : A → B) →
+    (x y : A) → (xy : x ≡ y : A) → f x ≡ f y : B =
+  λ A B ⇒ cong A (λ _ ⇒ B)
+
 def0 coherence :
     (A B : ★) → (AB : A ≡ B : ★) → (x : A) →
     Eq (𝑖 ⇒ AB @𝑖) x (coe (𝑖 ⇒ AB @𝑖) x) =
diff --git a/examples/nat.quox b/examples/nat.quox
index f52c768..3b9894a 100644
--- a/examples/nat.quox
+++ b/examples/nat.quox
@@ -4,12 +4,27 @@ load "either.quox";
 
 namespace nat {
 
+def elim-0-1 :
+    0.(P : ℕ → ★) →
+    ω.(P 0) → ω.(P 1) →
+    ω.(0.(n : ℕ) → P n → P (succ n)) →
+    (n : ℕ) → P n =
+  λ P p0 p1 ps n ⇒
+  case n return n' ⇒ P n' of {
+    zero    ⇒ p0;
+    succ n' ⇒
+      case n' return n'' ⇒ P (succ n'') of {
+        zero         ⇒ p1;
+        succ n'', IH ⇒ ps (succ n'') IH
+      }
+  }
+
 #[compile-scheme "(lambda (n) (cons n 'erased))"]
 def dup! : (n : ℕ) → [ω. Sing ℕ n] =
   λ n ⇒
   case n return n' ⇒ [ω. Sing ℕ n'] of {
     zero ⇒ [(zero, [δ _ ⇒ zero])];
-    succ n, 1.d ⇒
+    succ n, d ⇒
       appω (Sing ℕ n) (Sing ℕ (succ n))
         (sing.app ℕ ℕ n (λ n ⇒ succ n)) d
   };
@@ -21,16 +36,16 @@ def dup : ℕ → [ω.ℕ] =
 def plus : ℕ → ℕ → ℕ =
   λ m n ⇒
   case m return ℕ of {
-    zero        ⇒ n;
-    succ _, 1.p ⇒ succ p
+    zero      ⇒ n;
+    succ _, p ⇒ succ p
   };
 
 #[compile-scheme "(lambda% (m n) (* m n))"]
 def timesω : ℕ → ω.ℕ → ℕ =
   λ m n ⇒
   case m return ℕ of {
-    zero        ⇒ zero;
-    succ _, 1.t ⇒ plus n t
+    zero      ⇒ zero;
+    succ _, t ⇒ plus n t
   };
 
 def times : ℕ → ℕ → ℕ =
@@ -106,25 +121,42 @@ def eqb : ω.ℕ → ω.ℕ → Bool = λ m n ⇒ dec.bool (m ≡ n : ℕ) (eq?
 def0 plus-zero : (m : ℕ) → m ≡ plus m 0 : ℕ =
   λ m ⇒
   case m return m' ⇒ m' ≡ plus m' 0 : ℕ of {
-    zero         ⇒ δ _ ⇒ zero;
-    succ _, ω.ih ⇒ δ 𝑖 ⇒ succ (ih @𝑖)
+    zero        ⇒ δ _ ⇒ 0;
+    succ m', ih ⇒ δ 𝑖 ⇒ succ (ih @𝑖)
   };
 
 def0 plus-succ : (m n : ℕ) → succ (plus m n) ≡ plus m (succ n) : ℕ =
   λ m n ⇒
   case m return m' ⇒ succ (plus m' n) ≡ plus m' (succ n) : ℕ of {
-    zero         ⇒ δ _ ⇒ succ n;
-    succ _, ω.ih ⇒ δ 𝑖 ⇒ succ (ih @𝑖)
+    zero       ⇒ δ _ ⇒ succ n;
+    succ _, ih ⇒ δ 𝑖 ⇒ succ (ih @𝑖)
   };
 
 def0 plus-comm : (m n : ℕ) → plus m n ≡ plus n m : ℕ =
   λ m n ⇒
   case m return m' ⇒ plus m' n ≡ plus n m' : ℕ of {
     zero ⇒ plus-zero n;
-    succ m', ω.ih ⇒
+    succ m', ih ⇒
       trans ℕ (succ (plus m' n)) (succ (plus n m')) (plus n (succ m'))
         (δ 𝑖 ⇒ succ (ih @𝑖))
         (plus-succ n m')
   };
 
+def0 times-zero : (m : ℕ) → 0 ≡ timesω m 0 : ℕ =
+  λ m ⇒
+  case m return m' ⇒ 0 ≡ timesω m' 0 : ℕ of {
+    zero        ⇒ δ _ ⇒ zero;
+    succ m', ih ⇒ ih
+  };
+
+def0 times-succ : (m n : ℕ) → plus m (timesω m n) ≡ timesω m (succ n) : ℕ =
+  λ m n ⇒
+  case m
+  return m' ⇒ plus m' (timesω m' n) ≡ timesω m' (succ n) : ℕ
+  of {
+    zero ⇒ δ _ ⇒ 0;
+    succ m', ih ⇒
+      δ 𝑖 ⇒ plus (succ n) (ih @𝑖)
+  };
+
 }
diff --git a/examples/qty.quox b/examples/qty.quox
index 26a1a8b..9f5e529 100644
--- a/examples/qty.quox
+++ b/examples/qty.quox
@@ -61,13 +61,17 @@ def0 unbox : (π : Qty) → (A : ★) → Box π A → A =
     'any  ⇒ λ x ⇒ case x return A of { [x] ⇒ x };
   }
 
+def0 unbox0 = unbox 'zero
+def0 unbox1 = unbox 'one
+def0 unboxω = unbox 'any
+
 def apply : (π : Qty) → 0.(A : ★) → 0.(B : A → ★) →
             FUN π A B → (x : Box π A) → B (unbox π A x) =
   λ π A B ⇒
   case π
   return π' ⇒ FUN π' A B → (x : Box π' A) → B (unbox π' A x)
   of {
-    'zero ⇒ λ f x ⇒ case x return x' ⇒ B (unbox 'zero A x') of { [x] ⇒ f x };
-    'one  ⇒ λ f x ⇒ case x return x' ⇒ B (unbox 'one  A x') of { [x] ⇒ f x };
-    'any  ⇒ λ f x ⇒ case x return x' ⇒ B (unbox 'any  A x') of { [x] ⇒ f x };
+    'zero ⇒ λ f x ⇒ case x return x' ⇒ B (unbox0 A x') of { [x] ⇒ f x };
+    'one  ⇒ λ f x ⇒ case x return x' ⇒ B (unbox1 A x') of { [x] ⇒ f x };
+    'any  ⇒ λ f x ⇒ case x return x' ⇒ B (unboxω A x') of { [x] ⇒ f x };
   }