From 4206e655cd98174d570065c1677deb06f24b557d Mon Sep 17 00:00:00 2001
From: Victor Taelin <victor.taelin@gmail.com>
Date: Wed, 25 Sep 2024 10:32:23 -0300
Subject: [PATCH] stuff

---
 book/Bool/match.kind2  |  2 +-
 book/Equal/apply.kind2 |  2 +-
 book/Nat/_.kind2       | 14 +++++++-------
 book/Nat/add.kind2     |  4 ++--
 4 files changed, 11 insertions(+), 11 deletions(-)

diff --git a/book/Bool/match.kind2 b/book/Bool/match.kind2
index 8b9e2748c..b5393ccac 100644
--- a/book/Bool/match.kind2
+++ b/book/Bool/match.kind2
@@ -14,4 +14,4 @@ match
 - b: Bool
 : (P b)
 
-(~b P t f)
\ No newline at end of file
+(~b P t f)
diff --git a/book/Equal/apply.kind2 b/book/Equal/apply.kind2
index d5d9a209c..c092c3e53 100644
--- 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))
\ No newline at end of file
+}: (Equal B (f e.a) (f e.b))
diff --git a/book/Nat/_.kind2 b/book/Nat/_.kind2
index fd08d794e..06231cecb 100644
--- 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
index 15b9d978b..d4a38292a 100644
--- 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
-}
\ No newline at end of file
+}