stuff

HigherOrderCO · Sep 25, 2024 · 4206e65 · 4206e65
1 parent 2b6b5e7
commit 4206e65
Show file tree

Hide file tree

Showing 4 changed files with 11 additions and 11 deletions.
diff --git a/book/Bool/match.kind2 b/book/Bool/match.kind2
@@ -14,4 +14,4 @@ match
 - b: Bool
 : (P b)
 
-(~b P t f)
+(~b P t f)
diff --git a/book/Equal/apply.kind2 b/book/Equal/apply.kind2
@@ -16,4 +16,4 @@ apply <A: *> <B: *> <a: A> <b: A>
 
 match e {
   refl: ~λPλe(e (f e.a))
-}: (Equal B (f e.a) (f e.b))
+}: (Equal B (f e.a) (f e.b))
diff --git a/book/Nat/_.kind2 b/book/Nat/_.kind2
@@ -7,10 +7,10 @@ data Nat
 | succ (pred: Nat)
 | zero
 
-Nat
-: *
-= $(self: Nat)
-  ∀(P: ∀(n: Nat) *)
-  ∀(succ: ∀(n: Nat) (P (Nat/succ n)))
-  ∀(zero: (P Nat/zero))
-  (P self)
+//Nat
+//: *
+//= $(self: Nat)
+  //∀(P: ∀(n: Nat) *)
+  //∀(succ: ∀(n: Nat) (P (Nat/succ n)))
+  //∀(zero: (P Nat/zero))
+  //(P self)
diff --git a/book/Nat/add.kind2 b/book/Nat/add.kind2
@@ -11,6 +11,6 @@ add
 : Nat
 
 match a {
-  succ: (succ (add a.pred b))
+  succ: (succ (add add b))
   zero: b
-}
+}