add misc.refl, misc.sing, nat.minus

examples/misc.quox

@@ -32,6 +32,8 @@ def funext :
     (All A (eq-f A P p q)) → p ≡ q : All A P =
   λ A P p q eq ⇒ δ 𝑖 ⇒ λ x ⇒ eq x @𝑖
 
+def refl : 0.(A : ★) → (x : A) → x ≡ x : A = λ A x ⇒ δ _ ⇒ x
+
 def sym : 0.(A : ★) → 0.(x y : A) → (x ≡ y : A) → y ≡ x : A =
   λ A x y eq ⇒ δ 𝑖 ⇒ comp A (eq @0) @𝑖 { 0 𝑗 ⇒ eq @𝑗; 1 _ ⇒ eq @0 }
 
@@ -51,6 +53,9 @@ def0 HEq : (A B : ★) → A → B → ★¹ =
 def0 Sing : (A : ★) → A → ★ =
   λ A x ⇒ (val : A) × [0. val ≡ x : A]
 
+def sing : 0.(A : ★) → (x : A) → Sing A x =
+  λ A x ⇒ (x, [δ _ ⇒ x])
+
 namespace sing {
 
 def val : 0.(A : ★) → 0.(x : A) → Sing A x → A =

examples/nat.quox

@@ -44,6 +44,14 @@ def pred-succ : ω.(n : ℕ) → pred (succ n) ≡ n : ℕ =
 def0 succ-inj : (m n : ℕ) → succ m ≡ succ n : ℕ → m ≡ n : ℕ =
   λ m n eq ⇒ δ 𝑖 ⇒ pred (eq @𝑖);
 
+#[compile-scheme "(lambda% (m n) (max 0 (- m n)))"]
+def minus : ℕ → ℕ → ℕ =
+  λ m n ⇒
+  (case n return ℕ → ℕ of {
+    zero      ⇒ λ m ⇒ m;
+    succ _, f ⇒ λ m ⇒ f (pred m)
+  }) m;
+
 
 def0 IsSucc : ℕ → ★ =
   λ n ⇒ case n return ★ of { zero ⇒ False; succ _ ⇒ True };