From 5fdba77d04ac382de4877357002a7dae4710c5ce Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sat, 1 Apr 2023 19:16:30 +0200
Subject: [PATCH] nat example

---
 examples/nat.quox | 34 ++++++++++++++++++++++++++++++++++
 1 file changed, 34 insertions(+)
 create mode 100644 examples/nat.quox

diff --git a/examples/nat.quox b/examples/nat.quox
new file mode 100644
index 0000000..25c1c39
--- /dev/null
+++ b/examples/nat.quox
@@ -0,0 +1,34 @@
+defω dup-ℕ : 1.ℕ → [ω.ℕ] =
+  λ n ⇒
+  case1 n return [ω.ℕ] of {
+    zero ⇒ [zero];
+    succ _, 1.d ⇒
+      case1 d return [ω.ℕ] of { [d] ⇒ [succ d] }
+  };
+
+defω plus : 1.ℕ → 1.ℕ → ℕ =
+  λ m n ⇒
+  case1 m return ℕ of {
+    zero        ⇒ n;
+    succ _, 1.p ⇒ succ p
+  };
+
+defω times-ω : 1.ℕ → ω.ℕ → ℕ =
+  λ m n ⇒
+  case1 m return ℕ of {
+    zero        ⇒ zero;
+    succ _, 1.t ⇒ plus n t
+  };
+
+defω times : 1.ℕ → 1.ℕ → ℕ =
+  λ m n ⇒
+  case1 dup-ℕ n return ℕ of {
+    [n] ⇒ times-ω m n
+  };
+
+defω pred : 1.ℕ → ℕ =
+  λ n ⇒
+  case1 n return ℕ of { zero ⇒ zero; succ n ⇒ n };
+
+def0 pred-succ : ω.(n : ℕ) → pred (succ n) ≡ n : ℕ =
+  λ n ⇒ δ i ⇒ n;