some fixes and add BMap data structure

book/BMap.kind2

@@ -0,0 +1,3 @@
+data BMap A
+| node (lft: (BMap A)) (val: A) (rgt: (BMap A))
+| leaf

book/BMap/leaf.kind2

@@ -0,0 +1,3 @@
+BMap.leaf
+: ∀(A: *) (BMap A)
+= λA ~λP λnode λleaf leaf

book/BMap/node.kind2

@@ -0,0 +1,8 @@
+BMap.node
+: ∀(A: *)
+  ∀(lft: (BMap A))
+  ∀(val: A)
+  ∀(rgt: (BMap A))
+  (BMap A)
+= λA λlft λval λrgt
+  ~λP λnode λleaf (node lft val rgt)

book/Monad.kind2

@@ -12,3 +12,8 @@ Monad
     (P (Monad/new M bind pure))
   )
   (P self)
+
+//data Monad (M: * -> *)
+//| new
+    //(bind: ∀(A: *) ∀(B: *) ∀(a: (M A)) ∀(b: ∀(a: A) (M B)) (M B))
+    //(pure: ∀(A: *) ∀(a: A) (M A))

book/Nat/is_gtn.kind2

@@ -6,6 +6,6 @@ is_gtn (a: Nat) (b: Nat) : Bool =
     zero: false
     succ: match b {
       zero: true
-      succ: (gtn a.pred b.pred)
+      succ: (is_gtn a.pred b.pred)
     }
   }

book/Nat/is_ltn.kind2

@@ -9,6 +9,6 @@ is_ltn (a: Nat) (b: Nat) : Bool =
     }
     succ: match b {
       zero: false
-      succ: (ltn a.pred b.pred)
+      succ: (is_ltn a.pred b.pred)
     }
   }

book/Nat/is_ltn_or_eql.kind2

@@ -2,7 +2,7 @@ use Nat/{succ,zero}
 use Bool/{true,false}
 
 is_ltn_or_eql (a: Nat) (b: Nat) : Bool =
-  match _ = (Nat/ltn a b) {
+  match _ = (Nat/is_ltn a b) {
     true: true
     false: (Nat/equal a b)
   }