add more List and Nat functions

book/Bool/and.kind2

@@ -1,7 +1,7 @@
 use Bool/{true,false,and}
 
 and (a: Bool) (b: Bool) : Bool =
-  match b {
+  match a {
     true: b
     false: false
   }

book/List/and.kind2

@@ -0,0 +1,8 @@
+use List/{cons,nil}
+use Bool/{true}
+
+and (list: (List Bool)) : Bool =
+  fold list {
+    cons: (Bool/and list.head list.tail)
+    nil: true
+  }

book/List/drop.kind2

@@ -0,0 +1,11 @@
+use List/{cons,nil}
+use Nat/{succ,zero}
+
+drop <A> (n: Nat) (list: (List A)) : (List A) =
+  match n with (list: (List A)) {
+    zero: list
+    succ: match list {
+      cons: (drop n.pred list.tail)
+      nil: nil
+    }
+  }

book/List/filter.kind2

@@ -0,0 +1,10 @@
+use List/{cons,nil}
+
+filter <A> (cond: A -> Bool) (list: (List A)) : (List A) =
+  match list {
+    nil: nil
+    cons:
+      (Bool/if (cond list.head) (List A)
+        (cons list.head (filter cond list.tail))
+        (filter cond list.tail))
+  }

book/List/or.kind2

@@ -0,0 +1,8 @@
+use List/{cons,nil}
+use Bool/{false}
+
+or (list: (List Bool)) : Bool =
+  fold list {
+    cons: (Bool/or list.head list.tail)
+    nil: false
+  }

book/List/take.kind2

@@ -0,0 +1,11 @@
+use List/{cons,nil}
+use Nat/{succ,zero}
+
+take <A> (n: Nat) (list: (List A)) : (List A) =
+  match n with (list: (List A)) {
+    zero: nil
+    succ: match list {
+      cons: (cons list.head (take n.pred list.tail))
+      nil: nil
+    }
+  }

book/List/zip.kind2

@@ -0,0 +1,10 @@
+use List/{cons,nil}
+
+zip <A> <B> (as: (List A)) (bs: (List B)) : (List (Pair A B)) =
+  match as with (bs: (List B)) {
+    cons: match bs {
+      cons: (cons (Pair/new as.head bs.head) (zip as.tail bs.tail))
+      nil: nil
+    }
+    nil: nil
+  }

book/Monad.kind2

@@ -3,8 +3,8 @@ Monad
 = λM
   $(self: (Monad M))
   ∀(P: ∀(x: (Monad M)) *)
-  ∀(new: 
-    ∀(bind: 
+  ∀(new:
+    ∀(bind:
       ∀(A: *) ∀(B: *) ∀(a: (M A)) ∀(b: ∀(a: A) (M B))
       (M B)
     )

book/Nat/is_gtn.kind2

@@ -0,0 +1,11 @@
+use Nat/{succ,zero}
+use Bool/{true,false}
+
+is_gtn (a: Nat) (b: Nat) : Bool =
+  match a with (b: Nat) {
+    zero: false
+    succ: match b {
+      zero: true
+      succ: (gtn a.pred b.pred)
+    }
+  }

book/Nat/is_ltn.kind2

@@ -0,0 +1,14 @@
+use Nat/{succ,zero}
+use Bool/{true,false}
+
+is_ltn (a: Nat) (b: Nat) : Bool =
+  match a with (b: Nat) {
+    zero: match b {
+      zero: false
+      succ: true
+    }
+    succ: match b {
+      zero: false
+      succ: (ltn a.pred b.pred)
+    }
+  }

book/Nat/is_ltn_or_eql.kind2

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

book/Nat/mul.kind2

@@ -0,0 +1,7 @@
+use Nat/{succ,zero}
+
+mul (a: Nat) (b: Nat) : Nat =
+  match b {
+    succ: (Nat/add a (Nat/mul a b.pred))
+    zero: zero
+  }