diff --git a/book/Bool/and.kind2 b/book/Bool/and.kind2
index c57259414..1eb7f560e 100644
--- a/book/Bool/and.kind2
+++ b/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
}
diff --git a/book/List/and.kind2 b/book/List/and.kind2
new file mode 100644
index 000000000..abe1b8ddc
--- /dev/null
+++ b/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
+ }
diff --git a/book/List/drop.kind2 b/book/List/drop.kind2
new file mode 100644
index 000000000..7291e210e
--- /dev/null
+++ b/book/List/drop.kind2
@@ -0,0 +1,11 @@
+use List/{cons,nil}
+use Nat/{succ,zero}
+
+drop (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
+ }
+ }
diff --git a/book/List/filter.kind2 b/book/List/filter.kind2
new file mode 100644
index 000000000..d0a064cea
--- /dev/null
+++ b/book/List/filter.kind2
@@ -0,0 +1,10 @@
+use List/{cons,nil}
+
+filter (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))
+ }
diff --git a/book/List/or.kind2 b/book/List/or.kind2
new file mode 100644
index 000000000..aa3fb3a7b
--- /dev/null
+++ b/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
+ }
diff --git a/book/List/take.kind2 b/book/List/take.kind2
new file mode 100644
index 000000000..68fcdd7a2
--- /dev/null
+++ b/book/List/take.kind2
@@ -0,0 +1,11 @@
+use List/{cons,nil}
+use Nat/{succ,zero}
+
+take (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
+ }
+ }
diff --git a/book/List/zip.kind2 b/book/List/zip.kind2
new file mode 100644
index 000000000..ede3c569d
--- /dev/null
+++ b/book/List/zip.kind2
@@ -0,0 +1,10 @@
+use List/{cons,nil}
+
+zip (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
+ }
diff --git a/book/Monad.kind2 b/book/Monad.kind2
index 4095f8fbd..8fca9dbd3 100644
--- a/book/Monad.kind2
+++ b/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)
)
diff --git a/book/Nat/is_gtn.kind2 b/book/Nat/is_gtn.kind2
new file mode 100644
index 000000000..ea801a692
--- /dev/null
+++ 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)
+ }
+ }
diff --git a/book/Nat/is_ltn.kind2 b/book/Nat/is_ltn.kind2
new file mode 100644
index 000000000..7203c9871
--- /dev/null
+++ b/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)
+ }
+ }
diff --git a/book/Nat/is_ltn_or_eql.kind2 b/book/Nat/is_ltn_or_eql.kind2
new file mode 100644
index 000000000..e7e1abed2
--- /dev/null
+++ b/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)
+ }
diff --git a/book/Nat/mul.kind2 b/book/Nat/mul.kind2
new file mode 100644
index 000000000..53a6f7822
--- /dev/null
+++ 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
+ }