From 70288ef011777b851324ffa85c326b51a096171f Mon Sep 17 00:00:00 2001
From: Victor Taelin <victor.taelin@gmail.com>
Date: Fri, 15 Mar 2024 22:07:01 -0300
Subject: [PATCH] diff savida

---
 Cargo.lock                                    |   4 +-
 Cargo.toml                                    |   2 +-
 README.md                                     |  18 +--
 book/{BBT.balance.kind2 => BBT/balance.kind2} |   0
 .../balance/lft_heavier.kind2}                |   0
 .../balance/rgt_heavier.kind2}                |   0
 book/{BBT.bin.kind2 => BBT/bin.kind2}         |   0
 .../from_list.kind2}                          |   0
 book/{BBT.get.kind2 => BBT/get.kind2}         |   0
 book/{BBT.got.kind2 => BBT/got.kind2}         |   0
 .../got_size.kind2}                           |   0
 book/{BBT.has.kind2 => BBT/has.kind2}         |   0
 .../has/linear.kind2}                         |   0
 .../lft_rotate.kind2}                         |   0
 .../new_node.kind2}                           |   0
 .../rgt_rotate.kind2}                         |   0
 book/{BBT.set.kind2 => BBT/set.kind2}         |   0
 .../singleton.kind2}                          |   0
 book/{BBT.tip.kind2 => BBT/tip.kind2}         |   0
 book/{BBT.to_list.kind2 => BBT/to_list.kind2} |   0
 book/Bool.if.kind2                            |   5 -
 book/Bool.lemma.notnot.kind2                  |   7 -
 book/Bool.match.kind2                         |   7 -
 book/Bool.not.kind2                           |   7 -
 book/Bool.or.kind2                            |   7 -
 book/Bool.show.kind2                          |   5 -
 book/Bool.true.kind2                          |   2 -
 book/{Bool.and.kind2 => Bool/and.kind2}       |   2 +-
 book/{Bool.false.kind2 => Bool/false.kind2}   |   0
 book/Bool/if.kind2                            |   7 +
 book/Bool/lemma/double_negation.kind2         |   7 +
 book/Bool/match.kind2                         |   9 ++
 book/Bool/not.kind2                           |   7 +
 book/Bool/or.kind2                            |   7 +
 book/Bool/show.kind2                          |   7 +
 book/Bool/true.kind2                          |   2 +
 book/Char.equal.kind2                         |   2 -
 book/Char.escapes.kind2                       |  14 --
 book/Char.is_between.kind2                    |   5 -
 book/Char.is_blank.kind2                      |   2 -
 book/Char.is_decimal.kind2                    |   2 -
 book/Char.is_name.kind2                       |  21 ---
 book/Char.is_newline.kind2                    |   3 -
 book/Char.is_oper.kind2                       |  40 ------
 book/Char.is_slash.kind2                      |   3 -
 book/Char.slash.kind2                         |   3 -
 book/Char/equal.kind2                         |   2 +
 book/Char/escapes.kind2                       |  15 +++
 book/Char/is_between.kind2                    |   4 +
 book/Char/is_blank.kind2                      |   2 +
 book/Char/is_decimal.kind2                    |   2 +
 book/Char/is_name.kind2                       |  13 ++
 book/Char/is_newline.kind2                    |   2 +
 book/Char/is_oper.kind2                       |  18 +++
 book/Char/is_slash.kind2                      |   2 +
 book/Char/slash.kind2                         |   2 +
 book/Cmp.eql.kind2                            |   3 -
 book/Cmp.gtn.kind2                            |   3 -
 book/Cmp.is_gtn.kind2                         |   8 --
 book/Cmp.kind2                                |  12 +-
 book/Cmp.ltn.kind2                            |   3 -
 book/Cmp/eql.kind2                            |   2 +
 book/Cmp/gtn.kind2                            |   2 +
 book/Cmp/is_gtn.kind2                         |   9 ++
 book/Cmp/ltn.kind2                            |   2 +
 book/Empty.absurd.kind2                       |   3 -
 book/Empty.kind2                              |   4 +-
 book/Empty/absurd.kind2                       |   2 +
 book/Equal.kind2                              |   7 +
 book/Equal.refl.kind2                         |   4 -
 book/{Equal.apply.kind2 => Equal/apply.kind2} |   6 +-
 book/Equal/refl.kind2                         |   2 +
 book/{HVM.load.kind2 => HVM/load.kind2}       |   2 +-
 book/{HVM.log.kind2 => HVM/log.kind2}         |   0
 book/{HVM.print.kind2 => HVM/print.kind2}     |   0
 .../print/many.kind2}                         |   0
 book/{HVM.save.kind2 => HVM/save.kind2}       |   0
 book/{IO.bind.kind2 => IO/bind.kind2}         |   0
 book/{IO.done.kind2 => IO/done.kind2}         |   0
 book/{IO.load.kind2 => IO/load.kind2}         |   0
 book/{IO.load.do.kind2 => IO/load/do.kind2}   |   0
 book/{IO.print.kind2 => IO/print.kind2}       |   0
 book/{IO.print.do.kind2 => IO/print/do.kind2} |   0
 book/{IO.run.kind2 => IO/run.kind2}           |   0
 book/{IO.save.kind2 => IO/save.kind2}         |   0
 book/{IO.save.do.kind2 => IO/save/do.kind2}   |   0
 book/Kind.Text.show.go.kind2                  |   3 -
 .../API/check.kind2}                          |   0
 .../API/check/done.kind2}                     |   0
 .../API/get_refs.kind2}                       |   0
 .../API/normal.kind2}                         |   0
 book/{Kind.Binder.kind2 => Kind/Binder.kind2} |   0
 .../Binder/new.kind2}                         |   0
 book/{Kind.Book.kind2 => Kind/Book.kind2}     |   0
 .../Book/String.kind2}                        |   0
 .../Book/String/cons.kind2}                   |   0
 .../Book/String/nil.kind2}                    |   0
 .../Book/get_refs.kind2}                      |   2 +-
 .../Book/get_refs/go.kind2}                   |   6 +-
 .../Book/parse.kind2}                         |   0
 .../Book/parser.kind2}                        |   0
 .../Book/show.kind2}                          |   2 +-
 .../Book/show/go.kind2}                       |   6 +-
 book/{Kind.Oper.kind2 => Kind/Oper.kind2}     |   0
 .../Oper/add.kind2}                           |   0
 .../Oper/and.kind2}                           |   0
 .../Oper/div.kind2}                           |   0
 .../Oper/eq.kind2}                            |   0
 .../Oper/gt.kind2}                            |   0
 .../Oper/gte.kind2}                           |   0
 .../Oper/lsh.kind2}                           |   0
 .../Oper/lt.kind2}                            |   0
 .../Oper/lte.kind2}                           |   0
 .../Oper/mod.kind2}                           |   0
 .../Oper/mul.kind2}                           |   0
 .../Oper/ne.kind2}                            |   0
 .../Oper/or.kind2}                            |   0
 .../Oper/parser.kind2}                        |   0
 .../Oper/rsh.kind2}                           |   0
 .../Oper/show.kind2}                          |   2 +-
 .../Oper/show/go.kind2}                       |   4 +-
 .../Oper/sub.kind2}                           |   0
 .../Oper/xor.kind2}                           |   0
 .../PreTerm.kind2}                            |   0
 book/{Kind.Scope.kind2 => Kind/Scope.kind2}   |   0
 .../Scope/cons.kind2}                         |   0
 .../Scope/extend.kind2}                       |   0
 .../Scope/find.kind2}                         |   0
 .../Scope/nil.kind2}                          |   0
 book/{Kind.Term.kind2 => Kind/Term.kind2}     |   0
 .../Term/get_refs.kind2}                      |   2 +-
 .../Term/get_refs/go.kind2}                   |   4 +-
 .../Term/parse.kind2}                         |   0
 .../Term/parser.kind2}                        |   0
 .../Term/parser/all.kind2}                    |   0
 .../Term/parser/ann.kind2}                    |   0
 .../Term/parser/app.kind2}                    |   0
 .../Term/parser/bind.kind2}                   |   0
 .../Term/parser/chr.kind2}                    |   0
 .../Term/parser/def.kind2}                    |   0
 .../Term/parser/hol.kind2}                    |   0
 .../Term/parser/ins.kind2}                    |   0
 .../Term/parser/lam.kind2}                    |   0
 .../Term/parser/mat.kind2}                    |   0
 .../Term/parser/num.kind2}                    |   0
 .../Term/parser/op2.kind2}                    |   0
 .../Term/parser/pure.kind2}                   |   0
 .../Term/parser/set.kind2}                    |   0
 .../Term/parser/slf.kind2}                    |   0
 .../Term/parser/str.kind2}                    |   0
 .../Term/parser/u60.kind2}                    |   0
 .../Term/parser/var.kind2}                    |   0
 .../Term/show.kind2}                          |   2 +-
 .../Term/show/go.kind2}                       |   4 +-
 book/{Kind.Text.kind2 => Kind/Text.kind2}     |   0
 book/Kind/Text/show/go.kind2                  |   3 +
 book/{Kind.all.kind2 => Kind/all.kind2}       |   0
 book/{Kind.ann.kind2 => Kind/ann.kind2}       |   0
 book/{Kind.app.kind2 => Kind/app.kind2}       |   0
 book/{Kind.check.kind2 => Kind/check.kind2}   |   0
 .../comparer.kind2}                           |   0
 book/{Kind.def.kind2 => Kind/def.kind2}       |   0
 book/{Kind.equal.kind2 => Kind/equal.kind2}   |   0
 .../equal/enter.kind2}                        |   0
 .../equal/major.kind2}                        |   0
 .../equal/minor.kind2}                        |   0
 book/{Kind.export.kind2 => Kind/export.kind2} |   0
 book/{Kind.hol.kind2 => Kind/hol.kind2}       |   0
 .../identical.kind2}                          |   0
 book/{Kind.if.all.kind2 => Kind/if/all.kind2} |   0
 book/{Kind.if.ann.kind2 => Kind/if/ann.kind2} |   0
 book/{Kind.if.app.kind2 => Kind/if/app.kind2} |   0
 book/{Kind.if.def.kind2 => Kind/if/def.kind2} |   0
 book/{Kind.if.hol.kind2 => Kind/if/hol.kind2} |   0
 book/{Kind.if.ins.kind2 => Kind/if/ins.kind2} |   0
 book/{Kind.if.lam.kind2 => Kind/if/lam.kind2} |   0
 book/{Kind.if.mat.kind2 => Kind/if/mat.kind2} |   0
 book/{Kind.if.num.kind2 => Kind/if/num.kind2} |   0
 book/{Kind.if.op2.kind2 => Kind/if/op2.kind2} |   0
 book/{Kind.if.ref.kind2 => Kind/if/ref.kind2} |   0
 book/{Kind.if.set.kind2 => Kind/if/set.kind2} |   0
 book/{Kind.if.slf.kind2 => Kind/if/slf.kind2} |   0
 book/{Kind.if.txt.kind2 => Kind/if/txt.kind2} |   0
 book/{Kind.if.u60.kind2 => Kind/if/u60.kind2} |   0
 book/{Kind.if.var.kind2 => Kind/if/var.kind2} |   0
 book/{Kind.infer.kind2 => Kind/infer.kind2}   |   0
 book/{Kind.ins.kind2 => Kind/ins.kind2}       |   0
 book/{Kind.lam.kind2 => Kind/lam.kind2}       |   0
 book/{Kind.load.kind2 => Kind/load.kind2}     |   0
 .../load/code.kind2}                          |   0
 .../load/dependencies.kind2}                  |   0
 .../load/dependency.kind2}                    |   0
 .../load/name.kind2}                          |   0
 book/{Kind.mat.kind2 => Kind/mat.kind2}       |   0
 book/{Kind.normal.kind2 => Kind/normal.kind2} |   0
 .../normal/go.kind2}                          |   0
 book/{Kind.num.kind2 => Kind/num.kind2}       |   0
 book/{Kind.op2.kind2 => Kind/op2.kind2}       |   0
 book/{Kind.reduce.kind2 => Kind/reduce.kind2} |   0
 .../reduce/app.kind2}                         |   0
 .../reduce/mat.kind2}                         |   0
 .../reduce/op2.kind2}                         |   0
 .../reduce/ref.kind2}                         |   0
 .../reduce/txt.kind2}                         |   0
 book/{Kind.ref.kind2 => Kind/ref.kind2}       |   0
 book/{Kind.report.kind2 => Kind/report.kind2} |   0
 book/{Kind.set.kind2 => Kind/set.kind2}       |   0
 book/{Kind.skip.kind2 => Kind/skip.kind2}     |   0
 book/{Kind.slf.kind2 => Kind/slf.kind2}       |   0
 book/{Kind.txt.kind2 => Kind/txt.kind2}       |   0
 book/{Kind.u60.kind2 => Kind/u60.kind2}       |   0
 book/{Kind.var.kind2 => Kind/var.kind2}       |   0
 book/{Kind.verify.kind2 => Kind/verify.kind2} |   0
 book/List.Concatenator.build.kind2            |   3 -
 book/List.Concatenator.concat.kind2           |   6 -
 book/List.Concatenator.from_list.kind2        |  12 --
 book/List.Concatenator.join.kind2             |  13 --
 book/List.Concatenator.kind2                  |   3 -
 book/List.Concatenator.nil.kind2              |   3 -
 book/List.app.kind2                           |   8 --
 book/List.begin.kind2                         |  12 --
 book/List.concat.kind2                        |   7 -
 book/List.cons.kind2                          |   2 -
 book/List.find.kind2                          |  13 --
 book/List.fold.kind2                          |   7 -
 book/List.length.kind2                        |  10 --
 book/List.nil.kind2                           |   2 -
 book/List/Chunk.kind2                         |   2 +
 book/List/Chunk/build.kind2                   |   2 +
 book/List/Chunk/concat.kind2                  |   5 +
 book/List/Chunk/from_list.kind2               |   7 +
 book/List/Chunk/join.kind2                    |  17 +++
 book/List/Chunk/nil.kind2                     |   2 +
 book/{List.Church.kind2 => List/Church.kind2} |   0
 .../Church/cons.kind2}                        |   0
 .../Church/nil.kind2}                         |   0
 book/List/begin.kind2                         |  10 ++
 book/List/concat.kind2                        |   7 +
 book/List/cons.kind2                          |   2 +
 book/List/find.kind2                          |  12 ++
 book/List/fold.kind2                          |   7 +
 book/List/length.kind2                        |   8 ++
 book/{List.map.kind2 => List/map.kind2}       |   7 +-
 book/List/nil.kind2                           |   2 +
 book/List/sum.kind2                           |   5 +
 book/Maybe.bind.kind2                         |  11 --
 book/Maybe.kind2                              |  11 +-
 book/Maybe.monad.kind2                        |   3 -
 book/Maybe.none.kind2                         |   3 -
 book/Maybe.pure.kind2                         |   3 -
 book/Maybe.some.kind2                         |   3 -
 book/Maybe/bind.kind2                         |   7 +
 book/Maybe/monad.kind2                        |   3 +
 book/Maybe/none.kind2                         |   2 +
 book/Maybe/pure.kind2                         |   2 +
 book/Maybe/some.kind2                         |   2 +
 book/Monad.kind2                              |   4 +-
 book/{Monad.new.kind2 => Monad/new.kind2}     |   2 +-
 book/Nat.double.kind2                         |   8 --
 book/Nat.equal.kind2                          |  15 ---
 book/Nat.half.kind2                           |   8 --
 book/Nat.lemma.bft.kind2                      |   7 -
 book/Nat.succ.kind2                           |   3 -
 book/Nat.zero.kind2                           |   3 -
 book/{Nat.add.kind2 => Nat/add.kind2}         |   2 +-
 book/Nat/double.kind2                         |   7 +
 book/Nat/equal.kind2                          |  32 +++++
 book/Nat/half.kind2                           |  10 ++
 book/Nat/lemma/bft.kind2                      |   7 +
 book/Nat/succ.kind2                           |   2 +
 book/Nat/zero.kind2                           |   2 +
 book/Pair.fst.kind2                           |   5 -
 book/Pair.get.kind2                           |   8 --
 book/Pair.kind2                               |  11 +-
 book/Pair.new.kind2                           |   3 -
 book/Pair.snd.kind2                           |   5 -
 book/Pair/fst.kind2                           |   6 +
 book/Pair/get.kind2                           |   6 +
 book/Pair/new.kind2                           |   2 +
 book/Pair/snd.kind2                           |   6 +
 .../Guard.kind2}                              |   0
 .../Guard/get.kind2}                          |   0
 .../Guard/new.kind2}                          |   0
 .../Guard/pass.kind2}                         |   0
 .../Guard/text.kind2}                         |   0
 .../Result.kind2}                             |   0
 .../Result/done.kind2}                        |   0
 .../Result/fail.kind2}                        |   0
 book/{Parser.bind.kind2 => Parser/bind.kind2} |   0
 book/{Parser.char.kind2 => Parser/char.kind2} |   0
 .../decimal.kind2}                            |   0
 book/{Parser.fail.kind2 => Parser/fail.kind2} |   0
 .../is_eof.kind2}                             |   0
 book/{Parser.map.kind2 => Parser/map.kind2}   |   0
 book/{Parser.name.kind2 => Parser/name.kind2} |   0
 book/{Parser.oper.kind2 => Parser/oper.kind2} |   0
 book/{Parser.pick.kind2 => Parser/pick.kind2} |   0
 .../pick_while.kind2}                         |   0
 .../pick_while/go.kind2}                      |   0
 book/{Parser.pure.kind2 => Parser/pure.kind2} |   0
 .../repeat.kind2}                             |   0
 book/{Parser.skip.kind2 => Parser/skip.kind2} |   0
 book/{Parser.take.kind2 => Parser/take.kind2} |   0
 book/{Parser.test.kind2 => Parser/test.kind2} |   0
 book/{Parser.text.kind2 => Parser/text.kind2} |   0
 .../until.kind2}                              |   4 +-
 .../until/go.kind2}                           |  16 +--
 .../variant.kind2}                            |   0
 book/{QBool.false.kind2 => QBool/false.kind2} |   0
 book/{QBool.match.kind2 => QBool/match.kind2} |   0
 book/{QBool.true.kind2 => QBool/true.kind2}   |   0
 .../false.kind2}                              |   0
 .../match.kind2}                              |   0
 book/{QBool2.true.kind2 => QBool2/true.kind2} |   0
 book/{Sigma.new.kind2 => Sigma/new.kind2}     |   0
 book/String.Concatenator.build.kind2          |   3 -
 book/String.Concatenator.concat.kind2         |   4 -
 book/String.Concatenator.from_string.kind2    |   3 -
 book/String.Concatenator.join.kind2           |   3 -
 book/String.Concatenator.kind2                |   3 -
 book/String.Map.kind2                         |   3 -
 book/String.begin.kind2                       |   3 -
 book/String.concat.kind2                      |   3 -
 book/String.cons.kind2                        |   3 -
 book/String.indent.kind2                      |  11 --
 book/String.join.kind2                        |   7 -
 book/String.kind2                             |   5 +-
 book/String.length.kind2                      |   3 -
 book/String.newline.kind2                     |   3 -
 book/String.nil.kind2                         |   3 -
 book/String.skip.comment.kind2                |  11 --
 book/String.skip.kind2                        |  23 ----
 book/String.unpar.kind2                       |  11 --
 book/String.wrap.go.kind2                     |   7 -
 book/String.wrap.kind2                        |   4 -
 book/String/Chunk.kind2                       |   2 +
 book/String/Chunk/build.kind2                 |   3 +
 book/String/Chunk/concat.kind2                |   4 +
 book/String/Chunk/from_string.kind2           |   3 +
 book/String/Chunk/join.kind2                  |   3 +
 book/String/Map.kind2                         |   3 +
 .../Map/from_list.kind2}                      |   0
 .../Map/get.kind2}                            |   0
 .../Map/got.kind2}                            |   0
 .../Map/has.kind2}                            |   0
 .../Map/has/linear.kind2}                     |   0
 .../Map/new.kind2}                            |   0
 .../Map/set.kind2}                            |   0
 .../Map/to_list.kind2}                        |   0
 book/String/begin.kind2                       |   2 +
 book/{String.cmp.kind2 => String/cmp.kind2}   |  18 +--
 book/String/concat.kind2                      |   2 +
 book/String/cons.kind2                        |   2 +
 .../equal.kind2}                              |  18 ++-
 book/String/indent.kind2                      |   7 +
 book/String/join.kind2                        |   7 +
 .../join/go.kind2}                            |  10 +-
 book/String/length.kind2                      |   3 +
 book/String/newline.kind2                     |   3 +
 book/String/nil.kind2                         |   2 +
 .../quote.kind2}                              |   0
 book/String/skip.kind2                        |  23 ++++
 book/String/skip/comment.kind2                |  11 ++
 book/String/unpar.kind2                       |  11 ++
 book/String/wrap.kind2                        |   2 +
 book/String/wrap/go.kind2                     |   7 +
 book/The.kind2                                |  11 +-
 book/The.value.kind2                          |   7 -
 book/The/value.kind2                          |   2 +
 book/U60.Map.kind2                            |   3 -
 book/U60.abs_diff.kind2                       |   7 -
 book/U60.cmp.kind2                            |   9 --
 book/U60.equal.kind2                          |   7 -
 book/U60.from_nat.kind2                       |   7 -
 book/U60.if.kind2                             |   3 -
 book/U60.match.kind2                          |   8 --
 book/U60.max.kind2                            |   3 -
 book/U60.min.kind2                            |   3 -
 book/U60.name.kind2                           |   3 -
 book/U60.show.go.kind2                        |  11 --
 book/U60.show.kind2                           |   3 -
 book/U60.to_bool.kind2                        |   5 -
 book/U60/Map.kind2                            |   2 +
 book/U60/abs_diff.kind2                       |   7 +
 book/U60/cmp.kind2                            |   4 +
 book/U60/equal.kind2                          |   7 +
 book/{U60.fib.kind2 => U60/fib.kind2}         |   0
 book/U60/from_nat.kind2                       |   7 +
 book/U60/if.kind2                             |   5 +
 book/U60/match.kind2                          |   5 +
 book/U60/max.kind2                            |   5 +
 book/U60/min.kind2                            |   5 +
 book/U60/name.kind2                           |   2 +
 book/{U60.name.go.kind2 => U60/name/go.kind2} |   4 +-
 .../parser/decimal.kind2}                     |   0
 book/U60/show.kind2                           |   2 +
 book/U60/show/go.kind2                        |   5 +
 book/{U60.sum.kind2 => U60/sum.kind2}         |   0
 book/U60/to_bool.kind2                        |   7 +
 book/Unit.kind2                               |   6 +-
 book/Unit.match.kind2                         |   4 -
 book/Unit.one.kind2                           |   3 -
 book/Unit/match.kind2                         |   4 +
 book/Unit/new.kind2                           |   2 +
 book/Vector.cons.kind2                        |   3 -
 book/Vector.kind2                             |   4 +-
 book/Vector.nil.kind2                         |   3 -
 .../concat.kind2}                             |  10 +-
 book/Vector/cons.kind2                        |   2 +
 book/Vector/nil.kind2                         |   2 +
 book/script.js                                |  32 +++++
 src/book/mod.rs                               |  11 +-
 src/book/parse.rs                             | 102 ++++++++-------
 src/sugar/mod.rs                              | 122 +++++++++---------
 src/term/compile.rs                           |   2 +-
 src/term/mod.rs                               |   6 +-
 src/term/parse.rs                             |  18 +--
 src/term/show.rs                              |  14 +-
 418 files changed, 761 insertions(+), 823 deletions(-)
 rename book/{BBT.balance.kind2 => BBT/balance.kind2} (100%)
 rename book/{BBT.balance.lft_heavier.kind2 => BBT/balance/lft_heavier.kind2} (100%)
 rename book/{BBT.balance.rgt_heavier.kind2 => BBT/balance/rgt_heavier.kind2} (100%)
 rename book/{BBT.bin.kind2 => BBT/bin.kind2} (100%)
 rename book/{BBT.from_list.kind2 => BBT/from_list.kind2} (100%)
 rename book/{BBT.get.kind2 => BBT/get.kind2} (100%)
 rename book/{BBT.got.kind2 => BBT/got.kind2} (100%)
 rename book/{BBT.got_size.kind2 => BBT/got_size.kind2} (100%)
 rename book/{BBT.has.kind2 => BBT/has.kind2} (100%)
 rename book/{BBT.has.linear.kind2 => BBT/has/linear.kind2} (100%)
 rename book/{BBT.lft_rotate.kind2 => BBT/lft_rotate.kind2} (100%)
 rename book/{BBT.new_node.kind2 => BBT/new_node.kind2} (100%)
 rename book/{BBT.rgt_rotate.kind2 => BBT/rgt_rotate.kind2} (100%)
 rename book/{BBT.set.kind2 => BBT/set.kind2} (100%)
 rename book/{BBT.singleton.kind2 => BBT/singleton.kind2} (100%)
 rename book/{BBT.tip.kind2 => BBT/tip.kind2} (100%)
 rename book/{BBT.to_list.kind2 => BBT/to_list.kind2} (100%)
 delete mode 100644 book/Bool.if.kind2
 delete mode 100644 book/Bool.lemma.notnot.kind2
 delete mode 100644 book/Bool.match.kind2
 delete mode 100644 book/Bool.not.kind2
 delete mode 100644 book/Bool.or.kind2
 delete mode 100644 book/Bool.show.kind2
 delete mode 100644 book/Bool.true.kind2
 rename book/{Bool.and.kind2 => Bool/and.kind2} (75%)
 rename book/{Bool.false.kind2 => Bool/false.kind2} (100%)
 create mode 100644 book/Bool/if.kind2
 create mode 100644 book/Bool/lemma/double_negation.kind2
 create mode 100644 book/Bool/match.kind2
 create mode 100644 book/Bool/not.kind2
 create mode 100644 book/Bool/or.kind2
 create mode 100644 book/Bool/show.kind2
 create mode 100644 book/Bool/true.kind2
 delete mode 100644 book/Char.equal.kind2
 delete mode 100644 book/Char.escapes.kind2
 delete mode 100644 book/Char.is_between.kind2
 delete mode 100644 book/Char.is_blank.kind2
 delete mode 100644 book/Char.is_decimal.kind2
 delete mode 100644 book/Char.is_name.kind2
 delete mode 100644 book/Char.is_newline.kind2
 delete mode 100644 book/Char.is_oper.kind2
 delete mode 100644 book/Char.is_slash.kind2
 delete mode 100644 book/Char.slash.kind2
 create mode 100644 book/Char/equal.kind2
 create mode 100644 book/Char/escapes.kind2
 create mode 100644 book/Char/is_between.kind2
 create mode 100644 book/Char/is_blank.kind2
 create mode 100644 book/Char/is_decimal.kind2
 create mode 100644 book/Char/is_name.kind2
 create mode 100644 book/Char/is_newline.kind2
 create mode 100644 book/Char/is_oper.kind2
 create mode 100644 book/Char/is_slash.kind2
 create mode 100644 book/Char/slash.kind2
 delete mode 100644 book/Cmp.eql.kind2
 delete mode 100644 book/Cmp.gtn.kind2
 delete mode 100644 book/Cmp.is_gtn.kind2
 delete mode 100644 book/Cmp.ltn.kind2
 create mode 100644 book/Cmp/eql.kind2
 create mode 100644 book/Cmp/gtn.kind2
 create mode 100644 book/Cmp/is_gtn.kind2
 create mode 100644 book/Cmp/ltn.kind2
 delete mode 100644 book/Empty.absurd.kind2
 create mode 100644 book/Empty/absurd.kind2
 delete mode 100644 book/Equal.refl.kind2
 rename book/{Equal.apply.kind2 => Equal/apply.kind2} (64%)
 create mode 100644 book/Equal/refl.kind2
 rename book/{HVM.load.kind2 => HVM/load.kind2} (64%)
 rename book/{HVM.log.kind2 => HVM/log.kind2} (100%)
 rename book/{HVM.print.kind2 => HVM/print.kind2} (100%)
 rename book/{HVM.print.many.kind2 => HVM/print/many.kind2} (100%)
 rename book/{HVM.save.kind2 => HVM/save.kind2} (100%)
 rename book/{IO.bind.kind2 => IO/bind.kind2} (100%)
 rename book/{IO.done.kind2 => IO/done.kind2} (100%)
 rename book/{IO.load.kind2 => IO/load.kind2} (100%)
 rename book/{IO.load.do.kind2 => IO/load/do.kind2} (100%)
 rename book/{IO.print.kind2 => IO/print.kind2} (100%)
 rename book/{IO.print.do.kind2 => IO/print/do.kind2} (100%)
 rename book/{IO.run.kind2 => IO/run.kind2} (100%)
 rename book/{IO.save.kind2 => IO/save.kind2} (100%)
 rename book/{IO.save.do.kind2 => IO/save/do.kind2} (100%)
 delete mode 100644 book/Kind.Text.show.go.kind2
 rename book/{Kind.API.check.kind2 => Kind/API/check.kind2} (100%)
 rename book/{Kind.API.check.done.kind2 => Kind/API/check/done.kind2} (100%)
 rename book/{Kind.API.get_refs.kind2 => Kind/API/get_refs.kind2} (100%)
 rename book/{Kind.API.normal.kind2 => Kind/API/normal.kind2} (100%)
 rename book/{Kind.Binder.kind2 => Kind/Binder.kind2} (100%)
 rename book/{Kind.Binder.new.kind2 => Kind/Binder/new.kind2} (100%)
 rename book/{Kind.Book.kind2 => Kind/Book.kind2} (100%)
 rename book/{Kind.Book.String.kind2 => Kind/Book/String.kind2} (100%)
 rename book/{Kind.Book.String.cons.kind2 => Kind/Book/String/cons.kind2} (100%)
 rename book/{Kind.Book.String.nil.kind2 => Kind/Book/String/nil.kind2} (100%)
 rename book/{Kind.Book.get_refs.kind2 => Kind/Book/get_refs.kind2} (85%)
 rename book/{Kind.Book.get_refs.go.kind2 => Kind/Book/get_refs/go.kind2} (72%)
 rename book/{Kind.Book.parse.kind2 => Kind/Book/parse.kind2} (100%)
 rename book/{Kind.Book.parser.kind2 => Kind/Book/parser.kind2} (100%)
 rename book/{Kind.Book.show.kind2 => Kind/Book/show.kind2} (80%)
 rename book/{Kind.Book.show.go.kind2 => Kind/Book/show/go.kind2} (84%)
 rename book/{Kind.Oper.kind2 => Kind/Oper.kind2} (100%)
 rename book/{Kind.Oper.add.kind2 => Kind/Oper/add.kind2} (100%)
 rename book/{Kind.Oper.and.kind2 => Kind/Oper/and.kind2} (100%)
 rename book/{Kind.Oper.div.kind2 => Kind/Oper/div.kind2} (100%)
 rename book/{Kind.Oper.eq.kind2 => Kind/Oper/eq.kind2} (100%)
 rename book/{Kind.Oper.gt.kind2 => Kind/Oper/gt.kind2} (100%)
 rename book/{Kind.Oper.gte.kind2 => Kind/Oper/gte.kind2} (100%)
 rename book/{Kind.Oper.lsh.kind2 => Kind/Oper/lsh.kind2} (100%)
 rename book/{Kind.Oper.lt.kind2 => Kind/Oper/lt.kind2} (100%)
 rename book/{Kind.Oper.lte.kind2 => Kind/Oper/lte.kind2} (100%)
 rename book/{Kind.Oper.mod.kind2 => Kind/Oper/mod.kind2} (100%)
 rename book/{Kind.Oper.mul.kind2 => Kind/Oper/mul.kind2} (100%)
 rename book/{Kind.Oper.ne.kind2 => Kind/Oper/ne.kind2} (100%)
 rename book/{Kind.Oper.or.kind2 => Kind/Oper/or.kind2} (100%)
 rename book/{Kind.Oper.parser.kind2 => Kind/Oper/parser.kind2} (100%)
 rename book/{Kind.Oper.rsh.kind2 => Kind/Oper/rsh.kind2} (100%)
 rename book/{Kind.Oper.show.kind2 => Kind/Oper/show.kind2} (50%)
 rename book/{Kind.Oper.show.go.kind2 => Kind/Oper/show/go.kind2} (90%)
 rename book/{Kind.Oper.sub.kind2 => Kind/Oper/sub.kind2} (100%)
 rename book/{Kind.Oper.xor.kind2 => Kind/Oper/xor.kind2} (100%)
 rename book/{Kind.PreTerm.kind2 => Kind/PreTerm.kind2} (100%)
 rename book/{Kind.Scope.kind2 => Kind/Scope.kind2} (100%)
 rename book/{Kind.Scope.cons.kind2 => Kind/Scope/cons.kind2} (100%)
 rename book/{Kind.Scope.extend.kind2 => Kind/Scope/extend.kind2} (100%)
 rename book/{Kind.Scope.find.kind2 => Kind/Scope/find.kind2} (100%)
 rename book/{Kind.Scope.nil.kind2 => Kind/Scope/nil.kind2} (100%)
 rename book/{Kind.Term.kind2 => Kind/Term.kind2} (100%)
 rename book/{Kind.Term.get_refs.kind2 => Kind/Term/get_refs.kind2} (80%)
 rename book/{Kind.Term.get_refs.go.kind2 => Kind/Term/get_refs/go.kind2} (94%)
 rename book/{Kind.Term.parse.kind2 => Kind/Term/parse.kind2} (100%)
 rename book/{Kind.Term.parser.kind2 => Kind/Term/parser.kind2} (100%)
 rename book/{Kind.Term.parser.all.kind2 => Kind/Term/parser/all.kind2} (100%)
 rename book/{Kind.Term.parser.ann.kind2 => Kind/Term/parser/ann.kind2} (100%)
 rename book/{Kind.Term.parser.app.kind2 => Kind/Term/parser/app.kind2} (100%)
 rename book/{Kind.Term.parser.bind.kind2 => Kind/Term/parser/bind.kind2} (100%)
 rename book/{Kind.Term.parser.chr.kind2 => Kind/Term/parser/chr.kind2} (100%)
 rename book/{Kind.Term.parser.def.kind2 => Kind/Term/parser/def.kind2} (100%)
 rename book/{Kind.Term.parser.hol.kind2 => Kind/Term/parser/hol.kind2} (100%)
 rename book/{Kind.Term.parser.ins.kind2 => Kind/Term/parser/ins.kind2} (100%)
 rename book/{Kind.Term.parser.lam.kind2 => Kind/Term/parser/lam.kind2} (100%)
 rename book/{Kind.Term.parser.mat.kind2 => Kind/Term/parser/mat.kind2} (100%)
 rename book/{Kind.Term.parser.num.kind2 => Kind/Term/parser/num.kind2} (100%)
 rename book/{Kind.Term.parser.op2.kind2 => Kind/Term/parser/op2.kind2} (100%)
 rename book/{Kind.Term.parser.pure.kind2 => Kind/Term/parser/pure.kind2} (100%)
 rename book/{Kind.Term.parser.set.kind2 => Kind/Term/parser/set.kind2} (100%)
 rename book/{Kind.Term.parser.slf.kind2 => Kind/Term/parser/slf.kind2} (100%)
 rename book/{Kind.Term.parser.str.kind2 => Kind/Term/parser/str.kind2} (100%)
 rename book/{Kind.Term.parser.u60.kind2 => Kind/Term/parser/u60.kind2} (100%)
 rename book/{Kind.Term.parser.var.kind2 => Kind/Term/parser/var.kind2} (100%)
 rename book/{Kind.Term.show.kind2 => Kind/Term/show.kind2} (56%)
 rename book/{Kind.Term.show.go.kind2 => Kind/Term/show/go.kind2} (97%)
 rename book/{Kind.Text.kind2 => Kind/Text.kind2} (100%)
 create mode 100644 book/Kind/Text/show/go.kind2
 rename book/{Kind.all.kind2 => Kind/all.kind2} (100%)
 rename book/{Kind.ann.kind2 => Kind/ann.kind2} (100%)
 rename book/{Kind.app.kind2 => Kind/app.kind2} (100%)
 rename book/{Kind.check.kind2 => Kind/check.kind2} (100%)
 rename book/{Kind.comparer.kind2 => Kind/comparer.kind2} (100%)
 rename book/{Kind.def.kind2 => Kind/def.kind2} (100%)
 rename book/{Kind.equal.kind2 => Kind/equal.kind2} (100%)
 rename book/{Kind.equal.enter.kind2 => Kind/equal/enter.kind2} (100%)
 rename book/{Kind.equal.major.kind2 => Kind/equal/major.kind2} (100%)
 rename book/{Kind.equal.minor.kind2 => Kind/equal/minor.kind2} (100%)
 rename book/{Kind.export.kind2 => Kind/export.kind2} (100%)
 rename book/{Kind.hol.kind2 => Kind/hol.kind2} (100%)
 rename book/{Kind.identical.kind2 => Kind/identical.kind2} (100%)
 rename book/{Kind.if.all.kind2 => Kind/if/all.kind2} (100%)
 rename book/{Kind.if.ann.kind2 => Kind/if/ann.kind2} (100%)
 rename book/{Kind.if.app.kind2 => Kind/if/app.kind2} (100%)
 rename book/{Kind.if.def.kind2 => Kind/if/def.kind2} (100%)
 rename book/{Kind.if.hol.kind2 => Kind/if/hol.kind2} (100%)
 rename book/{Kind.if.ins.kind2 => Kind/if/ins.kind2} (100%)
 rename book/{Kind.if.lam.kind2 => Kind/if/lam.kind2} (100%)
 rename book/{Kind.if.mat.kind2 => Kind/if/mat.kind2} (100%)
 rename book/{Kind.if.num.kind2 => Kind/if/num.kind2} (100%)
 rename book/{Kind.if.op2.kind2 => Kind/if/op2.kind2} (100%)
 rename book/{Kind.if.ref.kind2 => Kind/if/ref.kind2} (100%)
 rename book/{Kind.if.set.kind2 => Kind/if/set.kind2} (100%)
 rename book/{Kind.if.slf.kind2 => Kind/if/slf.kind2} (100%)
 rename book/{Kind.if.txt.kind2 => Kind/if/txt.kind2} (100%)
 rename book/{Kind.if.u60.kind2 => Kind/if/u60.kind2} (100%)
 rename book/{Kind.if.var.kind2 => Kind/if/var.kind2} (100%)
 rename book/{Kind.infer.kind2 => Kind/infer.kind2} (100%)
 rename book/{Kind.ins.kind2 => Kind/ins.kind2} (100%)
 rename book/{Kind.lam.kind2 => Kind/lam.kind2} (100%)
 rename book/{Kind.load.kind2 => Kind/load.kind2} (100%)
 rename book/{Kind.load.code.kind2 => Kind/load/code.kind2} (100%)
 rename book/{Kind.load.dependencies.kind2 => Kind/load/dependencies.kind2} (100%)
 rename book/{Kind.load.dependency.kind2 => Kind/load/dependency.kind2} (100%)
 rename book/{Kind.load.name.kind2 => Kind/load/name.kind2} (100%)
 rename book/{Kind.mat.kind2 => Kind/mat.kind2} (100%)
 rename book/{Kind.normal.kind2 => Kind/normal.kind2} (100%)
 rename book/{Kind.normal.go.kind2 => Kind/normal/go.kind2} (100%)
 rename book/{Kind.num.kind2 => Kind/num.kind2} (100%)
 rename book/{Kind.op2.kind2 => Kind/op2.kind2} (100%)
 rename book/{Kind.reduce.kind2 => Kind/reduce.kind2} (100%)
 rename book/{Kind.reduce.app.kind2 => Kind/reduce/app.kind2} (100%)
 rename book/{Kind.reduce.mat.kind2 => Kind/reduce/mat.kind2} (100%)
 rename book/{Kind.reduce.op2.kind2 => Kind/reduce/op2.kind2} (100%)
 rename book/{Kind.reduce.ref.kind2 => Kind/reduce/ref.kind2} (100%)
 rename book/{Kind.reduce.txt.kind2 => Kind/reduce/txt.kind2} (100%)
 rename book/{Kind.ref.kind2 => Kind/ref.kind2} (100%)
 rename book/{Kind.report.kind2 => Kind/report.kind2} (100%)
 rename book/{Kind.set.kind2 => Kind/set.kind2} (100%)
 rename book/{Kind.skip.kind2 => Kind/skip.kind2} (100%)
 rename book/{Kind.slf.kind2 => Kind/slf.kind2} (100%)
 rename book/{Kind.txt.kind2 => Kind/txt.kind2} (100%)
 rename book/{Kind.u60.kind2 => Kind/u60.kind2} (100%)
 rename book/{Kind.var.kind2 => Kind/var.kind2} (100%)
 rename book/{Kind.verify.kind2 => Kind/verify.kind2} (100%)
 delete mode 100644 book/List.Concatenator.build.kind2
 delete mode 100644 book/List.Concatenator.concat.kind2
 delete mode 100644 book/List.Concatenator.from_list.kind2
 delete mode 100644 book/List.Concatenator.join.kind2
 delete mode 100644 book/List.Concatenator.kind2
 delete mode 100644 book/List.Concatenator.nil.kind2
 delete mode 100644 book/List.app.kind2
 delete mode 100644 book/List.begin.kind2
 delete mode 100644 book/List.concat.kind2
 delete mode 100644 book/List.cons.kind2
 delete mode 100644 book/List.find.kind2
 delete mode 100644 book/List.fold.kind2
 delete mode 100644 book/List.length.kind2
 delete mode 100644 book/List.nil.kind2
 create mode 100644 book/List/Chunk.kind2
 create mode 100644 book/List/Chunk/build.kind2
 create mode 100644 book/List/Chunk/concat.kind2
 create mode 100644 book/List/Chunk/from_list.kind2
 create mode 100644 book/List/Chunk/join.kind2
 create mode 100644 book/List/Chunk/nil.kind2
 rename book/{List.Church.kind2 => List/Church.kind2} (100%)
 rename book/{List.Church.cons.kind2 => List/Church/cons.kind2} (100%)
 rename book/{List.Church.nil.kind2 => List/Church/nil.kind2} (100%)
 create mode 100644 book/List/begin.kind2
 create mode 100644 book/List/concat.kind2
 create mode 100644 book/List/cons.kind2
 create mode 100644 book/List/find.kind2
 create mode 100644 book/List/fold.kind2
 create mode 100644 book/List/length.kind2
 rename book/{List.map.kind2 => List/map.kind2} (79%)
 create mode 100644 book/List/nil.kind2
 create mode 100644 book/List/sum.kind2
 delete mode 100644 book/Maybe.bind.kind2
 delete mode 100644 book/Maybe.monad.kind2
 delete mode 100644 book/Maybe.none.kind2
 delete mode 100644 book/Maybe.pure.kind2
 delete mode 100644 book/Maybe.some.kind2
 create mode 100644 book/Maybe/bind.kind2
 create mode 100644 book/Maybe/monad.kind2
 create mode 100644 book/Maybe/none.kind2
 create mode 100644 book/Maybe/pure.kind2
 create mode 100644 book/Maybe/some.kind2
 rename book/{Monad.new.kind2 => Monad/new.kind2} (95%)
 delete mode 100644 book/Nat.double.kind2
 delete mode 100644 book/Nat.equal.kind2
 delete mode 100644 book/Nat.half.kind2
 delete mode 100644 book/Nat.lemma.bft.kind2
 delete mode 100644 book/Nat.succ.kind2
 delete mode 100644 book/Nat.zero.kind2
 rename book/{Nat.add.kind2 => Nat/add.kind2} (81%)
 create mode 100644 book/Nat/double.kind2
 create mode 100644 book/Nat/equal.kind2
 create mode 100644 book/Nat/half.kind2
 create mode 100644 book/Nat/lemma/bft.kind2
 create mode 100644 book/Nat/succ.kind2
 create mode 100644 book/Nat/zero.kind2
 delete mode 100644 book/Pair.fst.kind2
 delete mode 100644 book/Pair.get.kind2
 delete mode 100644 book/Pair.new.kind2
 delete mode 100644 book/Pair.snd.kind2
 create mode 100644 book/Pair/fst.kind2
 create mode 100644 book/Pair/get.kind2
 create mode 100644 book/Pair/new.kind2
 create mode 100644 book/Pair/snd.kind2
 rename book/{Parser.Guard.kind2 => Parser/Guard.kind2} (100%)
 rename book/{Parser.Guard.get.kind2 => Parser/Guard/get.kind2} (100%)
 rename book/{Parser.Guard.new.kind2 => Parser/Guard/new.kind2} (100%)
 rename book/{Parser.Guard.pass.kind2 => Parser/Guard/pass.kind2} (100%)
 rename book/{Parser.Guard.text.kind2 => Parser/Guard/text.kind2} (100%)
 rename book/{Parser.Result.kind2 => Parser/Result.kind2} (100%)
 rename book/{Parser.Result.done.kind2 => Parser/Result/done.kind2} (100%)
 rename book/{Parser.Result.fail.kind2 => Parser/Result/fail.kind2} (100%)
 rename book/{Parser.bind.kind2 => Parser/bind.kind2} (100%)
 rename book/{Parser.char.kind2 => Parser/char.kind2} (100%)
 rename book/{Parser.decimal.kind2 => Parser/decimal.kind2} (100%)
 rename book/{Parser.fail.kind2 => Parser/fail.kind2} (100%)
 rename book/{Parser.is_eof.kind2 => Parser/is_eof.kind2} (100%)
 rename book/{Parser.map.kind2 => Parser/map.kind2} (100%)
 rename book/{Parser.name.kind2 => Parser/name.kind2} (100%)
 rename book/{Parser.oper.kind2 => Parser/oper.kind2} (100%)
 rename book/{Parser.pick.kind2 => Parser/pick.kind2} (100%)
 rename book/{Parser.pick_while.kind2 => Parser/pick_while.kind2} (100%)
 rename book/{Parser.pick_while.go.kind2 => Parser/pick_while/go.kind2} (100%)
 rename book/{Parser.pure.kind2 => Parser/pure.kind2} (100%)
 rename book/{Parser.repeat.kind2 => Parser/repeat.kind2} (100%)
 rename book/{Parser.skip.kind2 => Parser/skip.kind2} (100%)
 rename book/{Parser.take.kind2 => Parser/take.kind2} (100%)
 rename book/{Parser.test.kind2 => Parser/test.kind2} (100%)
 rename book/{Parser.text.kind2 => Parser/text.kind2} (100%)
 rename book/{Parser.until.kind2 => Parser/until.kind2} (76%)
 rename book/{Parser.until.go.kind2 => Parser/until/go.kind2} (51%)
 rename book/{Parser.variant.kind2 => Parser/variant.kind2} (100%)
 rename book/{QBool.false.kind2 => QBool/false.kind2} (100%)
 rename book/{QBool.match.kind2 => QBool/match.kind2} (100%)
 rename book/{QBool.true.kind2 => QBool/true.kind2} (100%)
 rename book/{QBool2.false.kind2 => QBool2/false.kind2} (100%)
 rename book/{QBool2.match.kind2 => QBool2/match.kind2} (100%)
 rename book/{QBool2.true.kind2 => QBool2/true.kind2} (100%)
 rename book/{Sigma.new.kind2 => Sigma/new.kind2} (100%)
 delete mode 100644 book/String.Concatenator.build.kind2
 delete mode 100644 book/String.Concatenator.concat.kind2
 delete mode 100644 book/String.Concatenator.from_string.kind2
 delete mode 100644 book/String.Concatenator.join.kind2
 delete mode 100644 book/String.Concatenator.kind2
 delete mode 100644 book/String.Map.kind2
 delete mode 100644 book/String.begin.kind2
 delete mode 100644 book/String.concat.kind2
 delete mode 100644 book/String.cons.kind2
 delete mode 100644 book/String.indent.kind2
 delete mode 100644 book/String.join.kind2
 delete mode 100644 book/String.length.kind2
 delete mode 100644 book/String.newline.kind2
 delete mode 100644 book/String.nil.kind2
 delete mode 100644 book/String.skip.comment.kind2
 delete mode 100644 book/String.skip.kind2
 delete mode 100644 book/String.unpar.kind2
 delete mode 100644 book/String.wrap.go.kind2
 delete mode 100644 book/String.wrap.kind2
 create mode 100644 book/String/Chunk.kind2
 create mode 100644 book/String/Chunk/build.kind2
 create mode 100644 book/String/Chunk/concat.kind2
 create mode 100644 book/String/Chunk/from_string.kind2
 create mode 100644 book/String/Chunk/join.kind2
 create mode 100644 book/String/Map.kind2
 rename book/{String.Map.from_list.kind2 => String/Map/from_list.kind2} (100%)
 rename book/{String.Map.get.kind2 => String/Map/get.kind2} (100%)
 rename book/{String.Map.got.kind2 => String/Map/got.kind2} (100%)
 rename book/{String.Map.has.kind2 => String/Map/has.kind2} (100%)
 rename book/{String.Map.has.linear.kind2 => String/Map/has/linear.kind2} (100%)
 rename book/{String.Map.new.kind2 => String/Map/new.kind2} (100%)
 rename book/{String.Map.set.kind2 => String/Map/set.kind2} (100%)
 rename book/{String.Map.to_list.kind2 => String/Map/to_list.kind2} (100%)
 create mode 100644 book/String/begin.kind2
 rename book/{String.cmp.kind2 => String/cmp.kind2} (55%)
 create mode 100644 book/String/concat.kind2
 create mode 100644 book/String/cons.kind2
 rename book/{String.equal.kind2 => String/equal.kind2} (50%)
 create mode 100644 book/String/indent.kind2
 create mode 100644 book/String/join.kind2
 rename book/{String.join.go.kind2 => String/join/go.kind2} (50%)
 create mode 100644 book/String/length.kind2
 create mode 100644 book/String/newline.kind2
 create mode 100644 book/String/nil.kind2
 rename book/{String.quote.kind2 => String/quote.kind2} (100%)
 create mode 100644 book/String/skip.kind2
 create mode 100644 book/String/skip/comment.kind2
 create mode 100644 book/String/unpar.kind2
 create mode 100644 book/String/wrap.kind2
 create mode 100644 book/String/wrap/go.kind2
 delete mode 100644 book/The.value.kind2
 create mode 100644 book/The/value.kind2
 delete mode 100644 book/U60.Map.kind2
 delete mode 100644 book/U60.abs_diff.kind2
 delete mode 100644 book/U60.cmp.kind2
 delete mode 100644 book/U60.equal.kind2
 delete mode 100644 book/U60.from_nat.kind2
 delete mode 100644 book/U60.if.kind2
 delete mode 100644 book/U60.match.kind2
 delete mode 100644 book/U60.max.kind2
 delete mode 100644 book/U60.min.kind2
 delete mode 100644 book/U60.name.kind2
 delete mode 100644 book/U60.show.go.kind2
 delete mode 100644 book/U60.show.kind2
 delete mode 100644 book/U60.to_bool.kind2
 create mode 100644 book/U60/Map.kind2
 create mode 100644 book/U60/abs_diff.kind2
 create mode 100644 book/U60/cmp.kind2
 create mode 100644 book/U60/equal.kind2
 rename book/{U60.fib.kind2 => U60/fib.kind2} (100%)
 create mode 100644 book/U60/from_nat.kind2
 create mode 100644 book/U60/if.kind2
 create mode 100644 book/U60/match.kind2
 create mode 100644 book/U60/max.kind2
 create mode 100644 book/U60/min.kind2
 create mode 100644 book/U60/name.kind2
 rename book/{U60.name.go.kind2 => U60/name/go.kind2} (71%)
 rename book/{U60.parser.decimal.kind2 => U60/parser/decimal.kind2} (100%)
 create mode 100644 book/U60/show.kind2
 create mode 100644 book/U60/show/go.kind2
 rename book/{U60.sum.kind2 => U60/sum.kind2} (100%)
 create mode 100644 book/U60/to_bool.kind2
 delete mode 100644 book/Unit.match.kind2
 delete mode 100644 book/Unit.one.kind2
 create mode 100644 book/Unit/match.kind2
 create mode 100644 book/Unit/new.kind2
 delete mode 100644 book/Vector.cons.kind2
 delete mode 100644 book/Vector.nil.kind2
 rename book/{Vector.concat.kind2 => Vector/concat.kind2} (70%)
 create mode 100644 book/Vector/cons.kind2
 create mode 100644 book/Vector/nil.kind2
 create mode 100644 book/script.js

diff --git a/Cargo.lock b/Cargo.lock
index e3af9f8c0..5d2b4191f 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -4,9 +4,9 @@ version = 3
 
 [[package]]
 name = "TSPL"
-version = "0.0.8"
+version = "0.0.9"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "1cf26cc6171f5f62baf926d04bc23eab3412598d76908fff83fda919bba486f0"
+checksum = "5a9423b1e6e2d6c0bbc03660f58f9c30f55359e13afea29432e6e767c0f7dc25"
 dependencies = [
  "highlight_error",
 ]
diff --git a/Cargo.toml b/Cargo.toml
index a1342c79f..0c3e6684f 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -8,7 +8,7 @@ name = "kind2"
 path = "src/main.rs"
 
 [dependencies]
-TSPL = "0.0.8"
+TSPL = "0.0.9"
 highlight_error = "0.1.1"
 im = "15.1.0"
 clap = "4.5.2"
diff --git a/README.md b/README.md
index 0f95bdc20..d4cc18e56 100644
--- a/README.md
+++ b/README.md
@@ -78,26 +78,22 @@ data List T
 | nil
 
 // Applies a function to all elements of a list
-map A B (f: ∀(x: A) B) (xs: (List A)) : (List B) =
-  match xs {
-    cons:
-      let head = (f xs.head)
-      let tail = (map _ _ f xs.tail)
-      (cons _ head tail)
-    nil:
-      []
+map <A> <B> (xs: (List A)) (f: A -> B) : (List B) =
+  fold xs {
+    ++: (f xs.head) ++ xs.tail
+    []: []
   }
 ```
 
 ### Theorems and Proofs:
 
 ```javascript
-use Nat.{succ,zero,half,double}
+use Nat/{succ,zero,half,double}
 
 // Proof that `∀n. n*2/2 = n`
-bft (n: Nat) : {(half (double n)) = n} =
+bft (n: Nat) : (half (double n)) == n =
   match n {
-    succ: (Equal.apply _ _ succ _ _ (bft n.pred))
+    succ: (Equal/apply succ (bft n.pred))
     zero: {=}
   }
 ```
diff --git a/book/BBT.balance.kind2 b/book/BBT/balance.kind2
similarity index 100%
rename from book/BBT.balance.kind2
rename to book/BBT/balance.kind2
diff --git a/book/BBT.balance.lft_heavier.kind2 b/book/BBT/balance/lft_heavier.kind2
similarity index 100%
rename from book/BBT.balance.lft_heavier.kind2
rename to book/BBT/balance/lft_heavier.kind2
diff --git a/book/BBT.balance.rgt_heavier.kind2 b/book/BBT/balance/rgt_heavier.kind2
similarity index 100%
rename from book/BBT.balance.rgt_heavier.kind2
rename to book/BBT/balance/rgt_heavier.kind2
diff --git a/book/BBT.bin.kind2 b/book/BBT/bin.kind2
similarity index 100%
rename from book/BBT.bin.kind2
rename to book/BBT/bin.kind2
diff --git a/book/BBT.from_list.kind2 b/book/BBT/from_list.kind2
similarity index 100%
rename from book/BBT.from_list.kind2
rename to book/BBT/from_list.kind2
diff --git a/book/BBT.get.kind2 b/book/BBT/get.kind2
similarity index 100%
rename from book/BBT.get.kind2
rename to book/BBT/get.kind2
diff --git a/book/BBT.got.kind2 b/book/BBT/got.kind2
similarity index 100%
rename from book/BBT.got.kind2
rename to book/BBT/got.kind2
diff --git a/book/BBT.got_size.kind2 b/book/BBT/got_size.kind2
similarity index 100%
rename from book/BBT.got_size.kind2
rename to book/BBT/got_size.kind2
diff --git a/book/BBT.has.kind2 b/book/BBT/has.kind2
similarity index 100%
rename from book/BBT.has.kind2
rename to book/BBT/has.kind2
diff --git a/book/BBT.has.linear.kind2 b/book/BBT/has/linear.kind2
similarity index 100%
rename from book/BBT.has.linear.kind2
rename to book/BBT/has/linear.kind2
diff --git a/book/BBT.lft_rotate.kind2 b/book/BBT/lft_rotate.kind2
similarity index 100%
rename from book/BBT.lft_rotate.kind2
rename to book/BBT/lft_rotate.kind2
diff --git a/book/BBT.new_node.kind2 b/book/BBT/new_node.kind2
similarity index 100%
rename from book/BBT.new_node.kind2
rename to book/BBT/new_node.kind2
diff --git a/book/BBT.rgt_rotate.kind2 b/book/BBT/rgt_rotate.kind2
similarity index 100%
rename from book/BBT.rgt_rotate.kind2
rename to book/BBT/rgt_rotate.kind2
diff --git a/book/BBT.set.kind2 b/book/BBT/set.kind2
similarity index 100%
rename from book/BBT.set.kind2
rename to book/BBT/set.kind2
diff --git a/book/BBT.singleton.kind2 b/book/BBT/singleton.kind2
similarity index 100%
rename from book/BBT.singleton.kind2
rename to book/BBT/singleton.kind2
diff --git a/book/BBT.tip.kind2 b/book/BBT/tip.kind2
similarity index 100%
rename from book/BBT.tip.kind2
rename to book/BBT/tip.kind2
diff --git a/book/BBT.to_list.kind2 b/book/BBT/to_list.kind2
similarity index 100%
rename from book/BBT.to_list.kind2
rename to book/BBT/to_list.kind2
diff --git a/book/Bool.if.kind2 b/book/Bool.if.kind2
deleted file mode 100644
index c957cc56b..000000000
--- a/book/Bool.if.kind2
+++ /dev/null
@@ -1,5 +0,0 @@
-Bool.if (b: Bool) (P: *) (t: P) (f: P) : P =
-  match b {
-    Bool.true: t
-    Bool.false: f
-  }
diff --git a/book/Bool.lemma.notnot.kind2 b/book/Bool.lemma.notnot.kind2
deleted file mode 100644
index 35effe2c8..000000000
--- a/book/Bool.lemma.notnot.kind2
+++ /dev/null
@@ -1,7 +0,0 @@
-use Bool.{true,false,not}
-
-notnot (x: Bool) : (not (not x)) == x =
-  match x {
-    true: {=}
-    false: {=}
-  }
diff --git a/book/Bool.match.kind2 b/book/Bool.match.kind2
deleted file mode 100644
index 35ec9b020..000000000
--- a/book/Bool.match.kind2
+++ /dev/null
@@ -1,7 +0,0 @@
-Bool.match
-  (b: Bool)
-  (P: ∀(x: Bool) *)
-  (t: (P Bool.true))
-  (f: (P Bool.false))
-: (P b)
-= (~b P t f)
diff --git a/book/Bool.not.kind2 b/book/Bool.not.kind2
deleted file mode 100644
index cf4ae7a4b..000000000
--- a/book/Bool.not.kind2
+++ /dev/null
@@ -1,7 +0,0 @@
-use Bool.{true,false}
-
-Bool.not (x: Bool) : Bool =
-  match x {
-    true: false
-    false: true
-  }
diff --git a/book/Bool.or.kind2 b/book/Bool.or.kind2
deleted file mode 100644
index 3d42e1cb4..000000000
--- a/book/Bool.or.kind2
+++ /dev/null
@@ -1,7 +0,0 @@
-use Bool.{true,false}
-
-Bool.or (a: Bool) (b: Bool) : Bool =
-  match a {
-    true: true
-    false: b
-  }
diff --git a/book/Bool.show.kind2 b/book/Bool.show.kind2
deleted file mode 100644
index d01458b4d..000000000
--- a/book/Bool.show.kind2
+++ /dev/null
@@ -1,5 +0,0 @@
-Bool.show (x: Bool) : String =
-  match x {
-    Bool.true: "true"
-    Bool.false: "false"
-  }
diff --git a/book/Bool.true.kind2 b/book/Bool.true.kind2
deleted file mode 100644
index 98228272e..000000000
--- a/book/Bool.true.kind2
+++ /dev/null
@@ -1,2 +0,0 @@
-Bool.true : Bool =
-  ~λP λt λf t
diff --git a/book/Bool.and.kind2 b/book/Bool/and.kind2
similarity index 75%
rename from book/Bool.and.kind2
rename to book/Bool/and.kind2
index 9f5135798..c57259414 100644
--- a/book/Bool.and.kind2
+++ b/book/Bool/and.kind2
@@ -1,4 +1,4 @@
-use Bool.{true,false,and}
+use Bool/{true,false,and}
 
 and (a: Bool) (b: Bool) : Bool =
   match b {
diff --git a/book/Bool.false.kind2 b/book/Bool/false.kind2
similarity index 100%
rename from book/Bool.false.kind2
rename to book/Bool/false.kind2
diff --git a/book/Bool/if.kind2 b/book/Bool/if.kind2
new file mode 100644
index 000000000..3a70fcd50
--- /dev/null
+++ b/book/Bool/if.kind2
@@ -0,0 +1,7 @@
+use Bool/{true,false}
+
+if (b: Bool) (P: *) (t: P) (f: P) : P =
+  match b {
+    true: t
+    false: f
+  }
diff --git a/book/Bool/lemma/double_negation.kind2 b/book/Bool/lemma/double_negation.kind2
new file mode 100644
index 000000000..8bf6575d7
--- /dev/null
+++ b/book/Bool/lemma/double_negation.kind2
@@ -0,0 +1,7 @@
+use Bool/{true,false,not}
+
+double_negation (x: Bool) : (not (not x)) == x =
+  match x {
+    true: {=}
+    false: {=}
+  }
diff --git a/book/Bool/match.kind2 b/book/Bool/match.kind2
new file mode 100644
index 000000000..088080bed
--- /dev/null
+++ b/book/Bool/match.kind2
@@ -0,0 +1,9 @@
+use Bool/{true,false}
+
+match
+  (b: Bool)
+  (P: ∀(x: Bool) *)
+  (t: (P true))
+  (f: (P false))
+: (P b)
+= (~b P t f)
diff --git a/book/Bool/not.kind2 b/book/Bool/not.kind2
new file mode 100644
index 000000000..39bdd0dd1
--- /dev/null
+++ b/book/Bool/not.kind2
@@ -0,0 +1,7 @@
+use Bool/{true,false}
+
+not (x: Bool) : Bool =
+  match x {
+    true: false
+    false: true
+  }
diff --git a/book/Bool/or.kind2 b/book/Bool/or.kind2
new file mode 100644
index 000000000..c847f174b
--- /dev/null
+++ b/book/Bool/or.kind2
@@ -0,0 +1,7 @@
+use Bool/{true,false}
+
+or (a: Bool) (b: Bool) : Bool =
+  match a {
+    true: true
+    false: b
+  }
diff --git a/book/Bool/show.kind2 b/book/Bool/show.kind2
new file mode 100644
index 000000000..7b8ae027e
--- /dev/null
+++ b/book/Bool/show.kind2
@@ -0,0 +1,7 @@
+use Bool/{true,false}
+
+show (x: Bool) : String =
+  match x {
+    true: "true"
+    false: "false"
+  }
diff --git a/book/Bool/true.kind2 b/book/Bool/true.kind2
new file mode 100644
index 000000000..dcc3aaa1b
--- /dev/null
+++ b/book/Bool/true.kind2
@@ -0,0 +1,2 @@
+true : Bool =
+  ~λP λt λf t
diff --git a/book/Char.equal.kind2 b/book/Char.equal.kind2
deleted file mode 100644
index 23e2b3a41..000000000
--- a/book/Char.equal.kind2
+++ /dev/null
@@ -1,2 +0,0 @@
-Char.equal (a: Char) (b: Char) : Bool =
-  (U60.equal a b)
diff --git a/book/Char.escapes.kind2 b/book/Char.escapes.kind2
deleted file mode 100644
index 470476f1d..000000000
--- a/book/Char.escapes.kind2
+++ /dev/null
@@ -1,14 +0,0 @@
-Char.escapes
-: (List (Pair Char Char))
-= [
-  (Pair.new _ _ 98 8)
-  (Pair.new _ _ 102 12)
-  (Pair.new _ _ 110 10)
-  (Pair.new _ _ 114 13)
-  (Pair.new _ _ 116 9)
-  (Pair.new _ _ 118 11)
-  (Pair.new _ _ 92 92)
-  (Pair.new _ _ 34 34)
-  (Pair.new _ _ 48 0)
-  (Pair.new _ _ 39 39)
-]
diff --git a/book/Char.is_between.kind2 b/book/Char.is_between.kind2
deleted file mode 100644
index f628e3435..000000000
--- a/book/Char.is_between.kind2
+++ /dev/null
@@ -1,5 +0,0 @@
-Char.is_between (min: Char) (max: Char) (chr: Char) : Bool
-= (Bool.and
-    (U60.to_bool (>= chr min))
-    (U60.to_bool (<= chr max))
-  )
diff --git a/book/Char.is_blank.kind2 b/book/Char.is_blank.kind2
deleted file mode 100644
index 84965bffa..000000000
--- a/book/Char.is_blank.kind2
+++ /dev/null
@@ -1,2 +0,0 @@
-Char.is_blank (a: Char) : Bool =
-  (Bool.or (Char.equal a 10) (Char.equal a 32))
diff --git a/book/Char.is_decimal.kind2 b/book/Char.is_decimal.kind2
deleted file mode 100644
index 89e7bfb0f..000000000
--- a/book/Char.is_decimal.kind2
+++ /dev/null
@@ -1,2 +0,0 @@
-Char.is_decimal (a: Char) : Bool =
-  (Char.is_between 48 57 a)
diff --git a/book/Char.is_name.kind2 b/book/Char.is_name.kind2
deleted file mode 100644
index 5635a167b..000000000
--- a/book/Char.is_name.kind2
+++ /dev/null
@@ -1,21 +0,0 @@
-Char.is_name
-: ∀(a: Char) Bool
-= λa
-  (Bool.or
-    (Char.is_between 97 122 a)
-    (Bool.or
-      (Char.is_between 65 90 a)
-      (Bool.or
-        (Char.is_between 48 57 a)
-        (Bool.or
-          (Char.equal 95 a)
-          (Bool.or
-            (Char.equal 46 a)
-            (Bool.or (Char.equal 45 a) Bool.false)
-          )
-        )
-      )
-    )
-  )
-
-
diff --git a/book/Char.is_newline.kind2 b/book/Char.is_newline.kind2
deleted file mode 100644
index f387899a0..000000000
--- a/book/Char.is_newline.kind2
+++ /dev/null
@@ -1,3 +0,0 @@
-Char.is_newline
-: ∀(a: Char) Bool
-= λa (Char.equal a 10)
\ No newline at end of file
diff --git a/book/Char.is_oper.kind2 b/book/Char.is_oper.kind2
deleted file mode 100644
index 4e152fa60..000000000
--- a/book/Char.is_oper.kind2
+++ /dev/null
@@ -1,40 +0,0 @@
-Char.is_oper
-: ∀(a: Char) Bool
-= λa
-  (Bool.or
-    (Char.equal 43 a)
-    (Bool.or
-      (Char.equal 45 a)
-      (Bool.or
-        (Char.equal 42 a)
-        (Bool.or
-          (Char.equal 47 a)
-          (Bool.or
-            (Char.equal 37 a)
-            (Bool.or
-              (Char.equal 60 a)
-              (Bool.or
-                (Char.equal 62 a)
-                (Bool.or
-                  (Char.equal 61 a)
-                  (Bool.or
-                    (Char.equal 38 a)
-                    (Bool.or
-                      (Char.equal 124 a)
-                      (Bool.or
-                        (Char.equal 94 a)
-                        (Bool.or
-                          (Char.equal 33 a)
-                          (Bool.or (Char.equal 126 a) Bool.false)
-                        )
-                      )
-                    )
-                  )
-                )
-              )
-            )
-          )
-        )
-      )
-    )
-  )
\ No newline at end of file
diff --git a/book/Char.is_slash.kind2 b/book/Char.is_slash.kind2
deleted file mode 100644
index 16f95aaef..000000000
--- a/book/Char.is_slash.kind2
+++ /dev/null
@@ -1,3 +0,0 @@
-Char.is_slash
-: ∀(a: Char) Bool
-= λa (Char.equal a 47)
\ No newline at end of file
diff --git a/book/Char.slash.kind2 b/book/Char.slash.kind2
deleted file mode 100644
index d01498556..000000000
--- a/book/Char.slash.kind2
+++ /dev/null
@@ -1,3 +0,0 @@
-Char.slash
-: Char
-= 47
\ No newline at end of file
diff --git a/book/Char/equal.kind2 b/book/Char/equal.kind2
new file mode 100644
index 000000000..e75c1fb36
--- /dev/null
+++ b/book/Char/equal.kind2
@@ -0,0 +1,2 @@
+equal (a: Char) (b: Char) : Bool =
+  (U60/equal a b)
diff --git a/book/Char/escapes.kind2 b/book/Char/escapes.kind2
new file mode 100644
index 000000000..3517f4152
--- /dev/null
+++ b/book/Char/escapes.kind2
@@ -0,0 +1,15 @@
+use Pair/{new}
+
+escapes : (List (Pair Char Char)) =
+  [
+    (new 98 8)
+    (new 102 12)
+    (new 110 10)
+    (new 114 13)
+    (new 116 9)
+    (new 118 11)
+    (new 92 92)
+    (new 34 34)
+    (new 48 0)
+    (new 39 39)
+  ]
diff --git a/book/Char/is_between.kind2 b/book/Char/is_between.kind2
new file mode 100644
index 000000000..57bc1baf1
--- /dev/null
+++ b/book/Char/is_between.kind2
@@ -0,0 +1,4 @@
+is_between (min: Char) (max: Char) (chr: Char) : Bool =
+  (Bool/and
+    (U60/to_bool (>= chr min))
+    (U60/to_bool (<= chr max)))
diff --git a/book/Char/is_blank.kind2 b/book/Char/is_blank.kind2
new file mode 100644
index 000000000..a894ab269
--- /dev/null
+++ b/book/Char/is_blank.kind2
@@ -0,0 +1,2 @@
+is_blank (a: Char) : Bool =
+  (Bool/or (Char/equal a 10) (Char/equal a 32))
diff --git a/book/Char/is_decimal.kind2 b/book/Char/is_decimal.kind2
new file mode 100644
index 000000000..df24aaad5
--- /dev/null
+++ b/book/Char/is_decimal.kind2
@@ -0,0 +1,2 @@
+is_decimal (a: Char) : Bool =
+  (Char/is_between 48 57 a)
diff --git a/book/Char/is_name.kind2 b/book/Char/is_name.kind2
new file mode 100644
index 000000000..46e5cdb36
--- /dev/null
+++ b/book/Char/is_name.kind2
@@ -0,0 +1,13 @@
+use Bool/{true,false,or}
+use Char/{is_between,equal}
+
+is_name (a: Char) : Bool =
+  (or (is_between 97 122 a)
+  (or (is_between 65 90 a)
+  (or (is_between 48 57 a)
+  (or (equal 95 a)
+  (or (equal 46 a)
+  (or (equal 45 a)
+  false))))))
+
+
diff --git a/book/Char/is_newline.kind2 b/book/Char/is_newline.kind2
new file mode 100644
index 000000000..21532c8a8
--- /dev/null
+++ b/book/Char/is_newline.kind2
@@ -0,0 +1,2 @@
+is_newline (a: Char) : Bool =
+  (Char/equal a 10)
diff --git a/book/Char/is_oper.kind2 b/book/Char/is_oper.kind2
new file mode 100644
index 000000000..649cd5a50
--- /dev/null
+++ b/book/Char/is_oper.kind2
@@ -0,0 +1,18 @@
+use Bool/{true,false,or}
+use Char/{equal}
+
+is_oper (a: Char) : Bool =
+  (or (equal 43 a)
+  (or (equal 45 a)
+  (or (equal 42 a)
+  (or (equal 47 a)
+  (or (equal 37 a)
+  (or (equal 60 a)
+  (or (equal 62 a)
+  (or (equal 61 a)
+  (or (equal 38 a)
+  (or (equal 124 a)
+  (or (equal 94 a)
+  (or (equal 33 a)
+  (or (equal 126 a)
+  false)))))))))))))
diff --git a/book/Char/is_slash.kind2 b/book/Char/is_slash.kind2
new file mode 100644
index 000000000..ac7d77233
--- /dev/null
+++ b/book/Char/is_slash.kind2
@@ -0,0 +1,2 @@
+is_slash (a: Char) : Bool =
+  (Char/equal a 47)
diff --git a/book/Char/slash.kind2 b/book/Char/slash.kind2
new file mode 100644
index 000000000..96198d995
--- /dev/null
+++ b/book/Char/slash.kind2
@@ -0,0 +1,2 @@
+slash : Char =
+  47
diff --git a/book/Cmp.eql.kind2 b/book/Cmp.eql.kind2
deleted file mode 100644
index b36580a1a..000000000
--- a/book/Cmp.eql.kind2
+++ /dev/null
@@ -1,3 +0,0 @@
-Cmp.eql
-: Cmp
-= ~λP λltn λeql λgtn eql
\ No newline at end of file
diff --git a/book/Cmp.gtn.kind2 b/book/Cmp.gtn.kind2
deleted file mode 100644
index 429b63b62..000000000
--- a/book/Cmp.gtn.kind2
+++ /dev/null
@@ -1,3 +0,0 @@
-Cmp.gtn
-: Cmp
-= ~λP λltn λeql λgtn gtn
\ No newline at end of file
diff --git a/book/Cmp.is_gtn.kind2 b/book/Cmp.is_gtn.kind2
deleted file mode 100644
index 50671fb49..000000000
--- a/book/Cmp.is_gtn.kind2
+++ /dev/null
@@ -1,8 +0,0 @@
-Cmp.is_gtn
-: ∀(cmp: Cmp) Bool
-= λcmp
-  use P = λx Bool
-  use ltn = Bool.false
-  use eql = Bool.false
-  use gtn = Bool.true
-  (~cmp P ltn eql gtn)
\ No newline at end of file
diff --git a/book/Cmp.kind2 b/book/Cmp.kind2
index e19386dd3..51507c407 100644
--- a/book/Cmp.kind2
+++ b/book/Cmp.kind2
@@ -1,8 +1,4 @@
-Cmp
-: *
-= $(self: Cmp)
-  ∀(P: ∀(cmp: Cmp) *)
-  ∀(ltn: (P Cmp.ltn))
-  ∀(eql: (P Cmp.eql))
-  ∀(gtn: (P Cmp.gtn))
-  (P self)
\ No newline at end of file
+data Cmp
+| ltn
+| eql
+| gtn
diff --git a/book/Cmp.ltn.kind2 b/book/Cmp.ltn.kind2
deleted file mode 100644
index 21dcfeb10..000000000
--- a/book/Cmp.ltn.kind2
+++ /dev/null
@@ -1,3 +0,0 @@
-Cmp.ltn
-: Cmp
-= ~λP λltn λeql λgtn ltn
\ No newline at end of file
diff --git a/book/Cmp/eql.kind2 b/book/Cmp/eql.kind2
new file mode 100644
index 000000000..fa6436a76
--- /dev/null
+++ b/book/Cmp/eql.kind2
@@ -0,0 +1,2 @@
+eql : Cmp =
+  ~λP λltn λeql λgtn eql
diff --git a/book/Cmp/gtn.kind2 b/book/Cmp/gtn.kind2
new file mode 100644
index 000000000..57288b82a
--- /dev/null
+++ b/book/Cmp/gtn.kind2
@@ -0,0 +1,2 @@
+Cmp.gtn : Cmp =
+  ~λP λltn λeql λgtn gtn
diff --git a/book/Cmp/is_gtn.kind2 b/book/Cmp/is_gtn.kind2
new file mode 100644
index 000000000..034c26c58
--- /dev/null
+++ b/book/Cmp/is_gtn.kind2
@@ -0,0 +1,9 @@
+use Bool/{true,false}
+use Cmp/{ltn,eql,gtn}
+
+Cmp.is_gtn (cmp: Cmp) : Bool =
+  match cmp {
+    ltn: false
+    eql: false
+    gtn: true
+  }
diff --git a/book/Cmp/ltn.kind2 b/book/Cmp/ltn.kind2
new file mode 100644
index 000000000..a9a1ac64c
--- /dev/null
+++ b/book/Cmp/ltn.kind2
@@ -0,0 +1,2 @@
+Cmp.ltn : Cmp =
+  ~λP λltn λeql λgtn ltn
diff --git a/book/Empty.absurd.kind2 b/book/Empty.absurd.kind2
deleted file mode 100644
index c829f0f0a..000000000
--- a/book/Empty.absurd.kind2
+++ /dev/null
@@ -1,3 +0,0 @@
-Empty.absurd
-: ∀(e: Empty) ∀(P: *) P
-= λe λP (~e λx P)
\ No newline at end of file
diff --git a/book/Empty.kind2 b/book/Empty.kind2
index 9db5bc69c..6c33e3179 100644
--- a/book/Empty.kind2
+++ b/book/Empty.kind2
@@ -1,3 +1 @@
-Empty
-: *
-= $(self: Empty) ∀(P: ∀(x: Empty) *) (P self)
\ No newline at end of file
+data Empty
diff --git a/book/Empty/absurd.kind2 b/book/Empty/absurd.kind2
new file mode 100644
index 000000000..ed478a9dd
--- /dev/null
+++ b/book/Empty/absurd.kind2
@@ -0,0 +1,2 @@
+absurd (e: Empty) (P: *) : P =
+  (~e λx(P))
diff --git a/book/Equal.kind2 b/book/Equal.kind2
index 99b11f0e5..6704dcf3b 100644
--- a/book/Equal.kind2
+++ b/book/Equal.kind2
@@ -1,6 +1,13 @@
 data Equal T (a: T) (b: T)
 | refl (a: T) : (Equal T a a)
 
+//Equal : ∀(T: *) ∀(a: T) ∀(b: T) * =
+  //λT λa λb
+  //$(self: (Equal T a b))
+  //∀(P: ∀(a: T) ∀(b: T) ∀(x: (Equal T a b)) *)
+  //∀(refl: ∀(x: T) (P x x (Equal/refl T x)))
+  //(P a b self)
+
 //Equal
 //: ∀(A: *) ∀(a: A) ∀(b: A) *
 //= λA λa λb ∀(P: ∀(x: A) *) ∀(p: (P a)) (P b)
diff --git a/book/Equal.refl.kind2 b/book/Equal.refl.kind2
deleted file mode 100644
index 4f865f0e6..000000000
--- a/book/Equal.refl.kind2
+++ /dev/null
@@ -1,4 +0,0 @@
-Equal.refl
-: ∀(A: *) ∀(x: A) (Equal A x x)
-= λA λx
-  ~ λP λrefl (refl x)
diff --git a/book/Equal.apply.kind2 b/book/Equal/apply.kind2
similarity index 64%
rename from book/Equal.apply.kind2
rename to book/Equal/apply.kind2
index 6e3270c73..a292e6cfe 100644
--- a/book/Equal.apply.kind2
+++ b/book/Equal/apply.kind2
@@ -1,8 +1,8 @@
-use Equal.{refl}
+//use Equal/{refl}
 
-apply <A> <B> <a> <b> (f: A -> B) (e: a == b) : (f a) == (f b) =
+apply <A: *> <B: *> <a: A> <b: B> (f: A -> B) (e: (Equal A a b)) : (Equal B (f a) (f b)) =
   match e {
-    refl: {=}
+    Equal/refl: {=}
   }
 
 
diff --git a/book/Equal/refl.kind2 b/book/Equal/refl.kind2
new file mode 100644
index 000000000..59b11233d
--- /dev/null
+++ b/book/Equal/refl.kind2
@@ -0,0 +1,2 @@
+refl <A> (x: A) : (Equal A x x) =
+  ~ λP λrefl (refl x)
diff --git a/book/HVM.load.kind2 b/book/HVM/load.kind2
similarity index 64%
rename from book/HVM.load.kind2
rename to book/HVM/load.kind2
index d7e6c05ac..a3e08d09a 100644
--- a/book/HVM.load.kind2
+++ b/book/HVM/load.kind2
@@ -1,3 +1,3 @@
 HVM.load
 : ∀(A: *) ∀(file: String) ∀(cont: ∀(x: String) A) A
-= λA λfile λcont (cont String.nil)
\ No newline at end of file
+= λA λfile λcont (cont String.nil)
diff --git a/book/HVM.log.kind2 b/book/HVM/log.kind2
similarity index 100%
rename from book/HVM.log.kind2
rename to book/HVM/log.kind2
diff --git a/book/HVM.print.kind2 b/book/HVM/print.kind2
similarity index 100%
rename from book/HVM.print.kind2
rename to book/HVM/print.kind2
diff --git a/book/HVM.print.many.kind2 b/book/HVM/print/many.kind2
similarity index 100%
rename from book/HVM.print.many.kind2
rename to book/HVM/print/many.kind2
diff --git a/book/HVM.save.kind2 b/book/HVM/save.kind2
similarity index 100%
rename from book/HVM.save.kind2
rename to book/HVM/save.kind2
diff --git a/book/IO.bind.kind2 b/book/IO/bind.kind2
similarity index 100%
rename from book/IO.bind.kind2
rename to book/IO/bind.kind2
diff --git a/book/IO.done.kind2 b/book/IO/done.kind2
similarity index 100%
rename from book/IO.done.kind2
rename to book/IO/done.kind2
diff --git a/book/IO.load.kind2 b/book/IO/load.kind2
similarity index 100%
rename from book/IO.load.kind2
rename to book/IO/load.kind2
diff --git a/book/IO.load.do.kind2 b/book/IO/load/do.kind2
similarity index 100%
rename from book/IO.load.do.kind2
rename to book/IO/load/do.kind2
diff --git a/book/IO.print.kind2 b/book/IO/print.kind2
similarity index 100%
rename from book/IO.print.kind2
rename to book/IO/print.kind2
diff --git a/book/IO.print.do.kind2 b/book/IO/print/do.kind2
similarity index 100%
rename from book/IO.print.do.kind2
rename to book/IO/print/do.kind2
diff --git a/book/IO.run.kind2 b/book/IO/run.kind2
similarity index 100%
rename from book/IO.run.kind2
rename to book/IO/run.kind2
diff --git a/book/IO.save.kind2 b/book/IO/save.kind2
similarity index 100%
rename from book/IO.save.kind2
rename to book/IO/save.kind2
diff --git a/book/IO.save.do.kind2 b/book/IO/save/do.kind2
similarity index 100%
rename from book/IO.save.do.kind2
rename to book/IO/save/do.kind2
diff --git a/book/Kind.Text.show.go.kind2 b/book/Kind.Text.show.go.kind2
deleted file mode 100644
index bcb2a7ad0..000000000
--- a/book/Kind.Text.show.go.kind2
+++ /dev/null
@@ -1,3 +0,0 @@
-Kind.Text.show.go
-: ∀(text: Kind.Text) String.Concatenator
-= String.Concatenator.from_string
\ No newline at end of file
diff --git a/book/Kind.API.check.kind2 b/book/Kind/API/check.kind2
similarity index 100%
rename from book/Kind.API.check.kind2
rename to book/Kind/API/check.kind2
diff --git a/book/Kind.API.check.done.kind2 b/book/Kind/API/check/done.kind2
similarity index 100%
rename from book/Kind.API.check.done.kind2
rename to book/Kind/API/check/done.kind2
diff --git a/book/Kind.API.get_refs.kind2 b/book/Kind/API/get_refs.kind2
similarity index 100%
rename from book/Kind.API.get_refs.kind2
rename to book/Kind/API/get_refs.kind2
diff --git a/book/Kind.API.normal.kind2 b/book/Kind/API/normal.kind2
similarity index 100%
rename from book/Kind.API.normal.kind2
rename to book/Kind/API/normal.kind2
diff --git a/book/Kind.Binder.kind2 b/book/Kind/Binder.kind2
similarity index 100%
rename from book/Kind.Binder.kind2
rename to book/Kind/Binder.kind2
diff --git a/book/Kind.Binder.new.kind2 b/book/Kind/Binder/new.kind2
similarity index 100%
rename from book/Kind.Binder.new.kind2
rename to book/Kind/Binder/new.kind2
diff --git a/book/Kind.Book.kind2 b/book/Kind/Book.kind2
similarity index 100%
rename from book/Kind.Book.kind2
rename to book/Kind/Book.kind2
diff --git a/book/Kind.Book.String.kind2 b/book/Kind/Book/String.kind2
similarity index 100%
rename from book/Kind.Book.String.kind2
rename to book/Kind/Book/String.kind2
diff --git a/book/Kind.Book.String.cons.kind2 b/book/Kind/Book/String/cons.kind2
similarity index 100%
rename from book/Kind.Book.String.cons.kind2
rename to book/Kind/Book/String/cons.kind2
diff --git a/book/Kind.Book.String.nil.kind2 b/book/Kind/Book/String/nil.kind2
similarity index 100%
rename from book/Kind.Book.String.nil.kind2
rename to book/Kind/Book/String/nil.kind2
diff --git a/book/Kind.Book.get_refs.kind2 b/book/Kind/Book/get_refs.kind2
similarity index 85%
rename from book/Kind.Book.get_refs.kind2
rename to book/Kind/Book/get_refs.kind2
index 5fd8e4175..f499d7753 100644
--- a/book/Kind.Book.get_refs.kind2
+++ b/book/Kind/Book/get_refs.kind2
@@ -1,7 +1,7 @@
 Kind.Book.get_refs
 : ∀(book: Kind.Book) (List String)
 = λbook
-  (List.Concatenator.build
+  (List.Chunk.build
     String
     (Kind.Book.get_refs.go
       (String.Map.to_list Kind.Term book)
diff --git a/book/Kind.Book.get_refs.go.kind2 b/book/Kind/Book/get_refs/go.kind2
similarity index 72%
rename from book/Kind.Book.get_refs.go.kind2
rename to book/Kind/Book/get_refs/go.kind2
index ab9c833ee..73a2ec584 100644
--- a/book/Kind.Book.get_refs.go.kind2
+++ b/book/Kind/Book/get_refs/go.kind2
@@ -1,10 +1,10 @@
 Kind.Book.get_refs.go
 : ∀(book: (List (Pair String Kind.Term)))
-  (List.Concatenator String)
+  (List.Chunk String)
 = λbook
-  use P = λx (List.Concatenator String)
+  use P = λx (List.Chunk String)
   use cons = λhead λtail
-    use P = λx (List.Concatenator String)
+    use P = λx (List.Chunk String)
     use new = λhead.fst λhead.snd λnil
       (Kind.Term.get_refs.go
         head.snd
diff --git a/book/Kind.Book.parse.kind2 b/book/Kind/Book/parse.kind2
similarity index 100%
rename from book/Kind.Book.parse.kind2
rename to book/Kind/Book/parse.kind2
diff --git a/book/Kind.Book.parser.kind2 b/book/Kind/Book/parser.kind2
similarity index 100%
rename from book/Kind.Book.parser.kind2
rename to book/Kind/Book/parser.kind2
diff --git a/book/Kind.Book.show.kind2 b/book/Kind/Book/show.kind2
similarity index 80%
rename from book/Kind.Book.show.kind2
rename to book/Kind/Book/show.kind2
index a0d42c19a..42678b2bb 100644
--- a/book/Kind.Book.show.kind2
+++ b/book/Kind/Book/show.kind2
@@ -1,6 +1,6 @@
 Kind.Book.show
 : ∀(book: Kind.Book) String
 = λbook
-  (String.Concatenator.build
+  (String.Chunk.build
     (Kind.Book.show.go (String.Map.to_list Kind.Term book))
   )
\ No newline at end of file
diff --git a/book/Kind.Book.show.go.kind2 b/book/Kind/Book/show/go.kind2
similarity index 84%
rename from book/Kind.Book.show.go.kind2
rename to book/Kind/Book/show/go.kind2
index 8a3b38476..787f20bac 100644
--- a/book/Kind.Book.show.go.kind2
+++ b/book/Kind/Book/show/go.kind2
@@ -1,10 +1,10 @@
 Kind.Book.show.go
 : ∀(book: (List (Pair String Kind.Term)))
-  String.Concatenator
+  String.Chunk
 = λbook
-  use P = λx String.Concatenator
+  use P = λx String.Chunk
   use cons = λhead λtail
-    use P = λx String.Concatenator
+    use P = λx String.Chunk
     use new = λhead.fst λhead.snd λnil
       (Kind.Text.show.go
         head.fst
diff --git a/book/Kind.Oper.kind2 b/book/Kind/Oper.kind2
similarity index 100%
rename from book/Kind.Oper.kind2
rename to book/Kind/Oper.kind2
diff --git a/book/Kind.Oper.add.kind2 b/book/Kind/Oper/add.kind2
similarity index 100%
rename from book/Kind.Oper.add.kind2
rename to book/Kind/Oper/add.kind2
diff --git a/book/Kind.Oper.and.kind2 b/book/Kind/Oper/and.kind2
similarity index 100%
rename from book/Kind.Oper.and.kind2
rename to book/Kind/Oper/and.kind2
diff --git a/book/Kind.Oper.div.kind2 b/book/Kind/Oper/div.kind2
similarity index 100%
rename from book/Kind.Oper.div.kind2
rename to book/Kind/Oper/div.kind2
diff --git a/book/Kind.Oper.eq.kind2 b/book/Kind/Oper/eq.kind2
similarity index 100%
rename from book/Kind.Oper.eq.kind2
rename to book/Kind/Oper/eq.kind2
diff --git a/book/Kind.Oper.gt.kind2 b/book/Kind/Oper/gt.kind2
similarity index 100%
rename from book/Kind.Oper.gt.kind2
rename to book/Kind/Oper/gt.kind2
diff --git a/book/Kind.Oper.gte.kind2 b/book/Kind/Oper/gte.kind2
similarity index 100%
rename from book/Kind.Oper.gte.kind2
rename to book/Kind/Oper/gte.kind2
diff --git a/book/Kind.Oper.lsh.kind2 b/book/Kind/Oper/lsh.kind2
similarity index 100%
rename from book/Kind.Oper.lsh.kind2
rename to book/Kind/Oper/lsh.kind2
diff --git a/book/Kind.Oper.lt.kind2 b/book/Kind/Oper/lt.kind2
similarity index 100%
rename from book/Kind.Oper.lt.kind2
rename to book/Kind/Oper/lt.kind2
diff --git a/book/Kind.Oper.lte.kind2 b/book/Kind/Oper/lte.kind2
similarity index 100%
rename from book/Kind.Oper.lte.kind2
rename to book/Kind/Oper/lte.kind2
diff --git a/book/Kind.Oper.mod.kind2 b/book/Kind/Oper/mod.kind2
similarity index 100%
rename from book/Kind.Oper.mod.kind2
rename to book/Kind/Oper/mod.kind2
diff --git a/book/Kind.Oper.mul.kind2 b/book/Kind/Oper/mul.kind2
similarity index 100%
rename from book/Kind.Oper.mul.kind2
rename to book/Kind/Oper/mul.kind2
diff --git a/book/Kind.Oper.ne.kind2 b/book/Kind/Oper/ne.kind2
similarity index 100%
rename from book/Kind.Oper.ne.kind2
rename to book/Kind/Oper/ne.kind2
diff --git a/book/Kind.Oper.or.kind2 b/book/Kind/Oper/or.kind2
similarity index 100%
rename from book/Kind.Oper.or.kind2
rename to book/Kind/Oper/or.kind2
diff --git a/book/Kind.Oper.parser.kind2 b/book/Kind/Oper/parser.kind2
similarity index 100%
rename from book/Kind.Oper.parser.kind2
rename to book/Kind/Oper/parser.kind2
diff --git a/book/Kind.Oper.rsh.kind2 b/book/Kind/Oper/rsh.kind2
similarity index 100%
rename from book/Kind.Oper.rsh.kind2
rename to book/Kind/Oper/rsh.kind2
diff --git a/book/Kind.Oper.show.kind2 b/book/Kind/Oper/show.kind2
similarity index 50%
rename from book/Kind.Oper.show.kind2
rename to book/Kind/Oper/show.kind2
index 1f510b72a..4d6312c05 100644
--- a/book/Kind.Oper.show.kind2
+++ b/book/Kind/Oper/show.kind2
@@ -1,4 +1,4 @@
 Kind.Oper.show
 : ∀(oper: Kind.Oper) String
 = λoper
-  (String.Concatenator.build (Kind.Oper.show.go oper))
\ No newline at end of file
+  (String.Chunk.build (Kind.Oper.show.go oper))
\ No newline at end of file
diff --git a/book/Kind.Oper.show.go.kind2 b/book/Kind/Oper/show/go.kind2
similarity index 90%
rename from book/Kind.Oper.show.go.kind2
rename to book/Kind/Oper/show/go.kind2
index 144c6b6c5..f77c325ea 100644
--- a/book/Kind.Oper.show.go.kind2
+++ b/book/Kind/Oper/show/go.kind2
@@ -1,7 +1,7 @@
 Kind.Oper.show.go
-: ∀(oper: Kind.Oper) String.Concatenator
+: ∀(oper: Kind.Oper) String.Chunk
 = λoper
-  use P = λX String.Concatenator
+  use P = λX String.Chunk
   use add = (Kind.Text.show.go "+")
   use mul = (Kind.Text.show.go "*")
   use sub = (Kind.Text.show.go "-")
diff --git a/book/Kind.Oper.sub.kind2 b/book/Kind/Oper/sub.kind2
similarity index 100%
rename from book/Kind.Oper.sub.kind2
rename to book/Kind/Oper/sub.kind2
diff --git a/book/Kind.Oper.xor.kind2 b/book/Kind/Oper/xor.kind2
similarity index 100%
rename from book/Kind.Oper.xor.kind2
rename to book/Kind/Oper/xor.kind2
diff --git a/book/Kind.PreTerm.kind2 b/book/Kind/PreTerm.kind2
similarity index 100%
rename from book/Kind.PreTerm.kind2
rename to book/Kind/PreTerm.kind2
diff --git a/book/Kind.Scope.kind2 b/book/Kind/Scope.kind2
similarity index 100%
rename from book/Kind.Scope.kind2
rename to book/Kind/Scope.kind2
diff --git a/book/Kind.Scope.cons.kind2 b/book/Kind/Scope/cons.kind2
similarity index 100%
rename from book/Kind.Scope.cons.kind2
rename to book/Kind/Scope/cons.kind2
diff --git a/book/Kind.Scope.extend.kind2 b/book/Kind/Scope/extend.kind2
similarity index 100%
rename from book/Kind.Scope.extend.kind2
rename to book/Kind/Scope/extend.kind2
diff --git a/book/Kind.Scope.find.kind2 b/book/Kind/Scope/find.kind2
similarity index 100%
rename from book/Kind.Scope.find.kind2
rename to book/Kind/Scope/find.kind2
diff --git a/book/Kind.Scope.nil.kind2 b/book/Kind/Scope/nil.kind2
similarity index 100%
rename from book/Kind.Scope.nil.kind2
rename to book/Kind/Scope/nil.kind2
diff --git a/book/Kind.Term.kind2 b/book/Kind/Term.kind2
similarity index 100%
rename from book/Kind.Term.kind2
rename to book/Kind/Term.kind2
diff --git a/book/Kind.Term.get_refs.kind2 b/book/Kind/Term/get_refs.kind2
similarity index 80%
rename from book/Kind.Term.get_refs.kind2
rename to book/Kind/Term/get_refs.kind2
index 41f5a42e8..f004f50cc 100644
--- a/book/Kind.Term.get_refs.kind2
+++ b/book/Kind/Term/get_refs.kind2
@@ -1,7 +1,7 @@
 Kind.Term.get_refs
 : ∀(term: Kind.Term) (List String)
 = λterm
-  (List.Concatenator.build
+  (List.Chunk.build
     String
     (Kind.Term.get_refs.go term)
   )
\ No newline at end of file
diff --git a/book/Kind.Term.get_refs.go.kind2 b/book/Kind/Term/get_refs/go.kind2
similarity index 94%
rename from book/Kind.Term.get_refs.go.kind2
rename to book/Kind/Term/get_refs/go.kind2
index 65b11f160..3f2a47ba4 100644
--- a/book/Kind.Term.get_refs.go.kind2
+++ b/book/Kind/Term/get_refs/go.kind2
@@ -1,7 +1,7 @@
 Kind.Term.get_refs.go
-: ∀(term: Kind.Term) (List.Concatenator String)
+: ∀(term: Kind.Term) (List.Chunk String)
 = λterm
-  use P = λx (List.Concatenator String)
+  use P = λx (List.Chunk String)
   use all = λnam λinp λbod λnil
     (Kind.Term.get_refs.go
       inp
diff --git a/book/Kind.Term.parse.kind2 b/book/Kind/Term/parse.kind2
similarity index 100%
rename from book/Kind.Term.parse.kind2
rename to book/Kind/Term/parse.kind2
diff --git a/book/Kind.Term.parser.kind2 b/book/Kind/Term/parser.kind2
similarity index 100%
rename from book/Kind.Term.parser.kind2
rename to book/Kind/Term/parser.kind2
diff --git a/book/Kind.Term.parser.all.kind2 b/book/Kind/Term/parser/all.kind2
similarity index 100%
rename from book/Kind.Term.parser.all.kind2
rename to book/Kind/Term/parser/all.kind2
diff --git a/book/Kind.Term.parser.ann.kind2 b/book/Kind/Term/parser/ann.kind2
similarity index 100%
rename from book/Kind.Term.parser.ann.kind2
rename to book/Kind/Term/parser/ann.kind2
diff --git a/book/Kind.Term.parser.app.kind2 b/book/Kind/Term/parser/app.kind2
similarity index 100%
rename from book/Kind.Term.parser.app.kind2
rename to book/Kind/Term/parser/app.kind2
diff --git a/book/Kind.Term.parser.bind.kind2 b/book/Kind/Term/parser/bind.kind2
similarity index 100%
rename from book/Kind.Term.parser.bind.kind2
rename to book/Kind/Term/parser/bind.kind2
diff --git a/book/Kind.Term.parser.chr.kind2 b/book/Kind/Term/parser/chr.kind2
similarity index 100%
rename from book/Kind.Term.parser.chr.kind2
rename to book/Kind/Term/parser/chr.kind2
diff --git a/book/Kind.Term.parser.def.kind2 b/book/Kind/Term/parser/def.kind2
similarity index 100%
rename from book/Kind.Term.parser.def.kind2
rename to book/Kind/Term/parser/def.kind2
diff --git a/book/Kind.Term.parser.hol.kind2 b/book/Kind/Term/parser/hol.kind2
similarity index 100%
rename from book/Kind.Term.parser.hol.kind2
rename to book/Kind/Term/parser/hol.kind2
diff --git a/book/Kind.Term.parser.ins.kind2 b/book/Kind/Term/parser/ins.kind2
similarity index 100%
rename from book/Kind.Term.parser.ins.kind2
rename to book/Kind/Term/parser/ins.kind2
diff --git a/book/Kind.Term.parser.lam.kind2 b/book/Kind/Term/parser/lam.kind2
similarity index 100%
rename from book/Kind.Term.parser.lam.kind2
rename to book/Kind/Term/parser/lam.kind2
diff --git a/book/Kind.Term.parser.mat.kind2 b/book/Kind/Term/parser/mat.kind2
similarity index 100%
rename from book/Kind.Term.parser.mat.kind2
rename to book/Kind/Term/parser/mat.kind2
diff --git a/book/Kind.Term.parser.num.kind2 b/book/Kind/Term/parser/num.kind2
similarity index 100%
rename from book/Kind.Term.parser.num.kind2
rename to book/Kind/Term/parser/num.kind2
diff --git a/book/Kind.Term.parser.op2.kind2 b/book/Kind/Term/parser/op2.kind2
similarity index 100%
rename from book/Kind.Term.parser.op2.kind2
rename to book/Kind/Term/parser/op2.kind2
diff --git a/book/Kind.Term.parser.pure.kind2 b/book/Kind/Term/parser/pure.kind2
similarity index 100%
rename from book/Kind.Term.parser.pure.kind2
rename to book/Kind/Term/parser/pure.kind2
diff --git a/book/Kind.Term.parser.set.kind2 b/book/Kind/Term/parser/set.kind2
similarity index 100%
rename from book/Kind.Term.parser.set.kind2
rename to book/Kind/Term/parser/set.kind2
diff --git a/book/Kind.Term.parser.slf.kind2 b/book/Kind/Term/parser/slf.kind2
similarity index 100%
rename from book/Kind.Term.parser.slf.kind2
rename to book/Kind/Term/parser/slf.kind2
diff --git a/book/Kind.Term.parser.str.kind2 b/book/Kind/Term/parser/str.kind2
similarity index 100%
rename from book/Kind.Term.parser.str.kind2
rename to book/Kind/Term/parser/str.kind2
diff --git a/book/Kind.Term.parser.u60.kind2 b/book/Kind/Term/parser/u60.kind2
similarity index 100%
rename from book/Kind.Term.parser.u60.kind2
rename to book/Kind/Term/parser/u60.kind2
diff --git a/book/Kind.Term.parser.var.kind2 b/book/Kind/Term/parser/var.kind2
similarity index 100%
rename from book/Kind.Term.parser.var.kind2
rename to book/Kind/Term/parser/var.kind2
diff --git a/book/Kind.Term.show.kind2 b/book/Kind/Term/show.kind2
similarity index 56%
rename from book/Kind.Term.show.kind2
rename to book/Kind/Term/show.kind2
index ded077ca4..a66d2cde4 100644
--- a/book/Kind.Term.show.kind2
+++ b/book/Kind/Term/show.kind2
@@ -1,4 +1,4 @@
 Kind.Term.show
 : ∀(term: Kind.Term) ∀(dep: Nat) String
 = λterm λdep
-  (String.Concatenator.build (Kind.Term.show.go term dep))
\ No newline at end of file
+  (String.Chunk.build (Kind.Term.show.go term dep))
\ No newline at end of file
diff --git a/book/Kind.Term.show.go.kind2 b/book/Kind/Term/show/go.kind2
similarity index 97%
rename from book/Kind.Term.show.go.kind2
rename to book/Kind/Term/show/go.kind2
index 5ea9d12db..9bdb7cfca 100644
--- a/book/Kind.Term.show.go.kind2
+++ b/book/Kind/Term/show/go.kind2
@@ -1,7 +1,7 @@
 Kind.Term.show.go
-: ∀(term: Kind.Term) ∀(dep: Nat) String.Concatenator
+: ∀(term: Kind.Term) ∀(dep: Nat) String.Chunk
 = λterm λdep
-  use P = λX String.Concatenator
+  use P = λX String.Chunk
   use all = λnam λinp λbod λnil
     (Kind.Text.show.go
       "∀("
diff --git a/book/Kind.Text.kind2 b/book/Kind/Text.kind2
similarity index 100%
rename from book/Kind.Text.kind2
rename to book/Kind/Text.kind2
diff --git a/book/Kind/Text/show/go.kind2 b/book/Kind/Text/show/go.kind2
new file mode 100644
index 000000000..0797e909a
--- /dev/null
+++ b/book/Kind/Text/show/go.kind2
@@ -0,0 +1,3 @@
+Kind.Text.show.go
+: ∀(text: Kind.Text) String.Chunk
+= String.Chunk.from_string
\ No newline at end of file
diff --git a/book/Kind.all.kind2 b/book/Kind/all.kind2
similarity index 100%
rename from book/Kind.all.kind2
rename to book/Kind/all.kind2
diff --git a/book/Kind.ann.kind2 b/book/Kind/ann.kind2
similarity index 100%
rename from book/Kind.ann.kind2
rename to book/Kind/ann.kind2
diff --git a/book/Kind.app.kind2 b/book/Kind/app.kind2
similarity index 100%
rename from book/Kind.app.kind2
rename to book/Kind/app.kind2
diff --git a/book/Kind.check.kind2 b/book/Kind/check.kind2
similarity index 100%
rename from book/Kind.check.kind2
rename to book/Kind/check.kind2
diff --git a/book/Kind.comparer.kind2 b/book/Kind/comparer.kind2
similarity index 100%
rename from book/Kind.comparer.kind2
rename to book/Kind/comparer.kind2
diff --git a/book/Kind.def.kind2 b/book/Kind/def.kind2
similarity index 100%
rename from book/Kind.def.kind2
rename to book/Kind/def.kind2
diff --git a/book/Kind.equal.kind2 b/book/Kind/equal.kind2
similarity index 100%
rename from book/Kind.equal.kind2
rename to book/Kind/equal.kind2
diff --git a/book/Kind.equal.enter.kind2 b/book/Kind/equal/enter.kind2
similarity index 100%
rename from book/Kind.equal.enter.kind2
rename to book/Kind/equal/enter.kind2
diff --git a/book/Kind.equal.major.kind2 b/book/Kind/equal/major.kind2
similarity index 100%
rename from book/Kind.equal.major.kind2
rename to book/Kind/equal/major.kind2
diff --git a/book/Kind.equal.minor.kind2 b/book/Kind/equal/minor.kind2
similarity index 100%
rename from book/Kind.equal.minor.kind2
rename to book/Kind/equal/minor.kind2
diff --git a/book/Kind.export.kind2 b/book/Kind/export.kind2
similarity index 100%
rename from book/Kind.export.kind2
rename to book/Kind/export.kind2
diff --git a/book/Kind.hol.kind2 b/book/Kind/hol.kind2
similarity index 100%
rename from book/Kind.hol.kind2
rename to book/Kind/hol.kind2
diff --git a/book/Kind.identical.kind2 b/book/Kind/identical.kind2
similarity index 100%
rename from book/Kind.identical.kind2
rename to book/Kind/identical.kind2
diff --git a/book/Kind.if.all.kind2 b/book/Kind/if/all.kind2
similarity index 100%
rename from book/Kind.if.all.kind2
rename to book/Kind/if/all.kind2
diff --git a/book/Kind.if.ann.kind2 b/book/Kind/if/ann.kind2
similarity index 100%
rename from book/Kind.if.ann.kind2
rename to book/Kind/if/ann.kind2
diff --git a/book/Kind.if.app.kind2 b/book/Kind/if/app.kind2
similarity index 100%
rename from book/Kind.if.app.kind2
rename to book/Kind/if/app.kind2
diff --git a/book/Kind.if.def.kind2 b/book/Kind/if/def.kind2
similarity index 100%
rename from book/Kind.if.def.kind2
rename to book/Kind/if/def.kind2
diff --git a/book/Kind.if.hol.kind2 b/book/Kind/if/hol.kind2
similarity index 100%
rename from book/Kind.if.hol.kind2
rename to book/Kind/if/hol.kind2
diff --git a/book/Kind.if.ins.kind2 b/book/Kind/if/ins.kind2
similarity index 100%
rename from book/Kind.if.ins.kind2
rename to book/Kind/if/ins.kind2
diff --git a/book/Kind.if.lam.kind2 b/book/Kind/if/lam.kind2
similarity index 100%
rename from book/Kind.if.lam.kind2
rename to book/Kind/if/lam.kind2
diff --git a/book/Kind.if.mat.kind2 b/book/Kind/if/mat.kind2
similarity index 100%
rename from book/Kind.if.mat.kind2
rename to book/Kind/if/mat.kind2
diff --git a/book/Kind.if.num.kind2 b/book/Kind/if/num.kind2
similarity index 100%
rename from book/Kind.if.num.kind2
rename to book/Kind/if/num.kind2
diff --git a/book/Kind.if.op2.kind2 b/book/Kind/if/op2.kind2
similarity index 100%
rename from book/Kind.if.op2.kind2
rename to book/Kind/if/op2.kind2
diff --git a/book/Kind.if.ref.kind2 b/book/Kind/if/ref.kind2
similarity index 100%
rename from book/Kind.if.ref.kind2
rename to book/Kind/if/ref.kind2
diff --git a/book/Kind.if.set.kind2 b/book/Kind/if/set.kind2
similarity index 100%
rename from book/Kind.if.set.kind2
rename to book/Kind/if/set.kind2
diff --git a/book/Kind.if.slf.kind2 b/book/Kind/if/slf.kind2
similarity index 100%
rename from book/Kind.if.slf.kind2
rename to book/Kind/if/slf.kind2
diff --git a/book/Kind.if.txt.kind2 b/book/Kind/if/txt.kind2
similarity index 100%
rename from book/Kind.if.txt.kind2
rename to book/Kind/if/txt.kind2
diff --git a/book/Kind.if.u60.kind2 b/book/Kind/if/u60.kind2
similarity index 100%
rename from book/Kind.if.u60.kind2
rename to book/Kind/if/u60.kind2
diff --git a/book/Kind.if.var.kind2 b/book/Kind/if/var.kind2
similarity index 100%
rename from book/Kind.if.var.kind2
rename to book/Kind/if/var.kind2
diff --git a/book/Kind.infer.kind2 b/book/Kind/infer.kind2
similarity index 100%
rename from book/Kind.infer.kind2
rename to book/Kind/infer.kind2
diff --git a/book/Kind.ins.kind2 b/book/Kind/ins.kind2
similarity index 100%
rename from book/Kind.ins.kind2
rename to book/Kind/ins.kind2
diff --git a/book/Kind.lam.kind2 b/book/Kind/lam.kind2
similarity index 100%
rename from book/Kind.lam.kind2
rename to book/Kind/lam.kind2
diff --git a/book/Kind.load.kind2 b/book/Kind/load.kind2
similarity index 100%
rename from book/Kind.load.kind2
rename to book/Kind/load.kind2
diff --git a/book/Kind.load.code.kind2 b/book/Kind/load/code.kind2
similarity index 100%
rename from book/Kind.load.code.kind2
rename to book/Kind/load/code.kind2
diff --git a/book/Kind.load.dependencies.kind2 b/book/Kind/load/dependencies.kind2
similarity index 100%
rename from book/Kind.load.dependencies.kind2
rename to book/Kind/load/dependencies.kind2
diff --git a/book/Kind.load.dependency.kind2 b/book/Kind/load/dependency.kind2
similarity index 100%
rename from book/Kind.load.dependency.kind2
rename to book/Kind/load/dependency.kind2
diff --git a/book/Kind.load.name.kind2 b/book/Kind/load/name.kind2
similarity index 100%
rename from book/Kind.load.name.kind2
rename to book/Kind/load/name.kind2
diff --git a/book/Kind.mat.kind2 b/book/Kind/mat.kind2
similarity index 100%
rename from book/Kind.mat.kind2
rename to book/Kind/mat.kind2
diff --git a/book/Kind.normal.kind2 b/book/Kind/normal.kind2
similarity index 100%
rename from book/Kind.normal.kind2
rename to book/Kind/normal.kind2
diff --git a/book/Kind.normal.go.kind2 b/book/Kind/normal/go.kind2
similarity index 100%
rename from book/Kind.normal.go.kind2
rename to book/Kind/normal/go.kind2
diff --git a/book/Kind.num.kind2 b/book/Kind/num.kind2
similarity index 100%
rename from book/Kind.num.kind2
rename to book/Kind/num.kind2
diff --git a/book/Kind.op2.kind2 b/book/Kind/op2.kind2
similarity index 100%
rename from book/Kind.op2.kind2
rename to book/Kind/op2.kind2
diff --git a/book/Kind.reduce.kind2 b/book/Kind/reduce.kind2
similarity index 100%
rename from book/Kind.reduce.kind2
rename to book/Kind/reduce.kind2
diff --git a/book/Kind.reduce.app.kind2 b/book/Kind/reduce/app.kind2
similarity index 100%
rename from book/Kind.reduce.app.kind2
rename to book/Kind/reduce/app.kind2
diff --git a/book/Kind.reduce.mat.kind2 b/book/Kind/reduce/mat.kind2
similarity index 100%
rename from book/Kind.reduce.mat.kind2
rename to book/Kind/reduce/mat.kind2
diff --git a/book/Kind.reduce.op2.kind2 b/book/Kind/reduce/op2.kind2
similarity index 100%
rename from book/Kind.reduce.op2.kind2
rename to book/Kind/reduce/op2.kind2
diff --git a/book/Kind.reduce.ref.kind2 b/book/Kind/reduce/ref.kind2
similarity index 100%
rename from book/Kind.reduce.ref.kind2
rename to book/Kind/reduce/ref.kind2
diff --git a/book/Kind.reduce.txt.kind2 b/book/Kind/reduce/txt.kind2
similarity index 100%
rename from book/Kind.reduce.txt.kind2
rename to book/Kind/reduce/txt.kind2
diff --git a/book/Kind.ref.kind2 b/book/Kind/ref.kind2
similarity index 100%
rename from book/Kind.ref.kind2
rename to book/Kind/ref.kind2
diff --git a/book/Kind.report.kind2 b/book/Kind/report.kind2
similarity index 100%
rename from book/Kind.report.kind2
rename to book/Kind/report.kind2
diff --git a/book/Kind.set.kind2 b/book/Kind/set.kind2
similarity index 100%
rename from book/Kind.set.kind2
rename to book/Kind/set.kind2
diff --git a/book/Kind.skip.kind2 b/book/Kind/skip.kind2
similarity index 100%
rename from book/Kind.skip.kind2
rename to book/Kind/skip.kind2
diff --git a/book/Kind.slf.kind2 b/book/Kind/slf.kind2
similarity index 100%
rename from book/Kind.slf.kind2
rename to book/Kind/slf.kind2
diff --git a/book/Kind.txt.kind2 b/book/Kind/txt.kind2
similarity index 100%
rename from book/Kind.txt.kind2
rename to book/Kind/txt.kind2
diff --git a/book/Kind.u60.kind2 b/book/Kind/u60.kind2
similarity index 100%
rename from book/Kind.u60.kind2
rename to book/Kind/u60.kind2
diff --git a/book/Kind.var.kind2 b/book/Kind/var.kind2
similarity index 100%
rename from book/Kind.var.kind2
rename to book/Kind/var.kind2
diff --git a/book/Kind.verify.kind2 b/book/Kind/verify.kind2
similarity index 100%
rename from book/Kind.verify.kind2
rename to book/Kind/verify.kind2
diff --git a/book/List.Concatenator.build.kind2 b/book/List.Concatenator.build.kind2
deleted file mode 100644
index e5e9df615..000000000
--- a/book/List.Concatenator.build.kind2
+++ /dev/null
@@ -1,3 +0,0 @@
-List.Concatenator.build
-: ∀(T: *) ∀(x: (List.Concatenator T)) (List T)
-= λT λx (x (List.nil T))
\ No newline at end of file
diff --git a/book/List.Concatenator.concat.kind2 b/book/List.Concatenator.concat.kind2
deleted file mode 100644
index 0fa20b2ca..000000000
--- a/book/List.Concatenator.concat.kind2
+++ /dev/null
@@ -1,6 +0,0 @@
-List.Concatenator.concat
-: ∀(T: *)
-  ∀(xs: (List.Concatenator T))
-  ∀(ys: (List.Concatenator T))
-  (List.Concatenator T)
-= λT λxs λys λnil (xs (ys nil))
\ No newline at end of file
diff --git a/book/List.Concatenator.from_list.kind2 b/book/List.Concatenator.from_list.kind2
deleted file mode 100644
index 657dd8935..000000000
--- a/book/List.Concatenator.from_list.kind2
+++ /dev/null
@@ -1,12 +0,0 @@
-List.Concatenator.from_list
-: ∀(T: *) ∀(xs: (List T)) (List.Concatenator T)
-= λT λxs
-  use P = λxs (List.Concatenator T)
-  use cons = λhead λtail λnil
-    (List.cons
-      T
-      head
-      (List.Concatenator.from_list T tail nil)
-    )
-  use nil = λnil nil
-  (~xs P cons nil)
\ No newline at end of file
diff --git a/book/List.Concatenator.join.kind2 b/book/List.Concatenator.join.kind2
deleted file mode 100644
index e4af9ce39..000000000
--- a/book/List.Concatenator.join.kind2
+++ /dev/null
@@ -1,13 +0,0 @@
-List.Concatenator.join
-: ∀(T: *) ∀(xs: (List (List.Concatenator T)))
-  (List.Concatenator T)
-= λT λxs
-  use P = λxs (List.Concatenator T)
-  use cons = λhead λtail
-    (List.Concatenator.concat
-      T
-      head
-      (List.Concatenator.join T tail)
-    )
-  use nil = (List.Concatenator.nil T)
-  (~xs P cons nil)
\ No newline at end of file
diff --git a/book/List.Concatenator.kind2 b/book/List.Concatenator.kind2
deleted file mode 100644
index 5e1009868..000000000
--- a/book/List.Concatenator.kind2
+++ /dev/null
@@ -1,3 +0,0 @@
-List.Concatenator
-: ∀(T: *) *
-= λT ∀(nil: (List T)) (List T)
\ No newline at end of file
diff --git a/book/List.Concatenator.nil.kind2 b/book/List.Concatenator.nil.kind2
deleted file mode 100644
index ce104602d..000000000
--- a/book/List.Concatenator.nil.kind2
+++ /dev/null
@@ -1,3 +0,0 @@
-List.Concatenator.nil
-: ∀(T: *) (List.Concatenator T)
-= λT λx x
\ No newline at end of file
diff --git a/book/List.app.kind2 b/book/List.app.kind2
deleted file mode 100644
index 34686bea9..000000000
--- a/book/List.app.kind2
+++ /dev/null
@@ -1,8 +0,0 @@
-List.app
-: ∀(A: *) ∀(B: *) ∀(f: ∀(x: A) B) ∀(x: (List A))
-  (List B)
-= λA λB λf λx
-  use P = λx (List B)
-  use cons = λh λt (List.cons B (f h) (List.app A B f t))
-  use nil = (List.nil B)
-  (~x P cons nil)
\ No newline at end of file
diff --git a/book/List.begin.kind2 b/book/List.begin.kind2
deleted file mode 100644
index c3e2c7aec..000000000
--- a/book/List.begin.kind2
+++ /dev/null
@@ -1,12 +0,0 @@
-List.begin
-: ∀(A: *) ∀(list: (List A)) (List A)
-= λA λlist
-  use P = λx (List A)
-  use cons = λx0 λxs
-    use P = λx (List A)
-    use cons = λx1 λxs
-      (List.cons A x0 (List.begin A (List.cons A x1 xs)))
-    use nil = (List.nil A)
-    (~xs P cons nil)
-  use nil = (List.nil A)
-  (~list P cons nil)
\ No newline at end of file
diff --git a/book/List.concat.kind2 b/book/List.concat.kind2
deleted file mode 100644
index fad8bc326..000000000
--- a/book/List.concat.kind2
+++ /dev/null
@@ -1,7 +0,0 @@
-use List.{cons,nil}
-
-concat (T: *) (xs: (List T)) (ys: (List T)) : (List T) =
-  match xs {
-    cons: (cons T xs.head (concat T xs.tail ys))
-    nil: ys
-  }
diff --git a/book/List.cons.kind2 b/book/List.cons.kind2
deleted file mode 100644
index 7c1fee91d..000000000
--- a/book/List.cons.kind2
+++ /dev/null
@@ -1,2 +0,0 @@
-List.cons <T> (head: T) (tail: (List T)) : (List T) =
-  ~λP λcons λnil (cons head tail)
diff --git a/book/List.find.kind2 b/book/List.find.kind2
deleted file mode 100644
index 2f9e540fb..000000000
--- a/book/List.find.kind2
+++ /dev/null
@@ -1,13 +0,0 @@
-List.find
-: ∀(A: *) ∀(cond: ∀(x: A) Bool) ∀(list: (List A))
-  (Maybe A)
-= λA λcond λlist
-  use P = λx (Maybe A)
-  use cons = λhead λtail
-    use found = (cond head)
-    use P = λx (Maybe A)
-    use true = (Maybe.some A head)
-    use false = (List.find A cond tail)
-    (~found P true false)
-  use nil = (Maybe.none A)
-  (~list P cons nil)
\ No newline at end of file
diff --git a/book/List.fold.kind2 b/book/List.fold.kind2
deleted file mode 100644
index 85b97072d..000000000
--- a/book/List.fold.kind2
+++ /dev/null
@@ -1,7 +0,0 @@
-use List.{cons,nil}
-
-List.fold <A> <B> (xs: (List A)) (c: A -> B -> B) (n: B) : B =
-  match xs {
-    cons: (c xs.head (List.fold xs.tail c n))
-    nil: n
-  }
diff --git a/book/List.length.kind2 b/book/List.length.kind2
deleted file mode 100644
index 4917cab81..000000000
--- a/book/List.length.kind2
+++ /dev/null
@@ -1,10 +0,0 @@
-use List.{cons,nil}
-use Nat.{succ,zero}
-
-length A (xs: (List A)) : Nat =
-  match xs {
-    cons:
-      (succ (length A xs.tail))
-    nil:
-      zero
-  }
diff --git a/book/List.nil.kind2 b/book/List.nil.kind2
deleted file mode 100644
index 1231de8e3..000000000
--- a/book/List.nil.kind2
+++ /dev/null
@@ -1,2 +0,0 @@
-List.nil <T> : (List T) =
-  ~λP λcons λnil nil
diff --git a/book/List/Chunk.kind2 b/book/List/Chunk.kind2
new file mode 100644
index 000000000..dfa5d1aa4
--- /dev/null
+++ b/book/List/Chunk.kind2
@@ -0,0 +1,2 @@
+List.Chunk (T: *) : * =
+  ∀(nil: (List T)) (List T)
diff --git a/book/List/Chunk/build.kind2 b/book/List/Chunk/build.kind2
new file mode 100644
index 000000000..f87837ae1
--- /dev/null
+++ b/book/List/Chunk/build.kind2
@@ -0,0 +1,2 @@
+build <T> (x: (List/Chunk T)) : (List T) =
+  (x [])
diff --git a/book/List/Chunk/concat.kind2 b/book/List/Chunk/concat.kind2
new file mode 100644
index 000000000..a8f554d56
--- /dev/null
+++ b/book/List/Chunk/concat.kind2
@@ -0,0 +1,5 @@
+concat <T>
+  (xs: (List/Chunk T))
+  (ys: (List/Chunk T))
+: (List/Chunk T) =
+  λnil (xs (ys nil))
diff --git a/book/List/Chunk/from_list.kind2 b/book/List/Chunk/from_list.kind2
new file mode 100644
index 000000000..91ea74dd5
--- /dev/null
+++ b/book/List/Chunk/from_list.kind2
@@ -0,0 +1,7 @@
+use List/{cons,nil}
+
+from_list <T> (xs: (List T)) : (List/Chunk T) =
+  match xs {
+    ++: λnil (cons xs.head (from_list xs.tail nil))
+    []: λnil nil
+  }
diff --git a/book/List/Chunk/join.kind2 b/book/List/Chunk/join.kind2
new file mode 100644
index 000000000..da90b0e3f
--- /dev/null
+++ b/book/List/Chunk/join.kind2
@@ -0,0 +1,17 @@
+use List/{cons,nil}
+
+join <T> (xs: (List (List/Chunk T))) : (List/Chunk T) =
+  match xs {
+    ++: (List/Chunk/concat xs.head (join xs.tail))
+    []: List/Chunk/nil
+  }
+  
+  //use P = λxs (List.Chunk T)
+  //use cons = λhead λtail
+    //(List.Chunk.concat
+      //T
+      //head
+      //(List.Chunk.join T tail)
+    //)
+  //use nil = (List.Chunk.nil T)
+  //(~xs P cons nil)
diff --git a/book/List/Chunk/nil.kind2 b/book/List/Chunk/nil.kind2
new file mode 100644
index 000000000..19ff5963d
--- /dev/null
+++ b/book/List/Chunk/nil.kind2
@@ -0,0 +1,2 @@
+nil <T> : (List/Chunk T) =
+  λnil nil
diff --git a/book/List.Church.kind2 b/book/List/Church.kind2
similarity index 100%
rename from book/List.Church.kind2
rename to book/List/Church.kind2
diff --git a/book/List.Church.cons.kind2 b/book/List/Church/cons.kind2
similarity index 100%
rename from book/List.Church.cons.kind2
rename to book/List/Church/cons.kind2
diff --git a/book/List.Church.nil.kind2 b/book/List/Church/nil.kind2
similarity index 100%
rename from book/List.Church.nil.kind2
rename to book/List/Church/nil.kind2
diff --git a/book/List/begin.kind2 b/book/List/begin.kind2
new file mode 100644
index 000000000..dafd140c0
--- /dev/null
+++ b/book/List/begin.kind2
@@ -0,0 +1,10 @@
+use List/{cons,nil}
+
+begin <A> (xs: (List A)) : (List A) =
+  match xs {
+    ++: match xs.tail {
+      ++: (cons xs.head (begin (cons xs.tail.head xs.tail)))
+      []: []
+    }
+    []: []
+  }
diff --git a/book/List/concat.kind2 b/book/List/concat.kind2
new file mode 100644
index 000000000..6f4540aa7
--- /dev/null
+++ b/book/List/concat.kind2
@@ -0,0 +1,7 @@
+use List/{cons,nil}
+
+concat <T> (xs: (List T)) (ys: (List T)) : (List T) =
+  match xs {
+    ++: (cons xs.head (concat xs.tail ys))
+    []: ys
+  }
diff --git a/book/List/cons.kind2 b/book/List/cons.kind2
new file mode 100644
index 000000000..b1a84b3f4
--- /dev/null
+++ b/book/List/cons.kind2
@@ -0,0 +1,2 @@
+cons <T> (head: T) (tail: (List T)) : (List T) =
+  ~λP λcons λnil (cons head tail)
diff --git a/book/List/find.kind2 b/book/List/find.kind2
new file mode 100644
index 000000000..632a2b2cc
--- /dev/null
+++ b/book/List/find.kind2
@@ -0,0 +1,12 @@
+use Bool/{true,false}
+use List/{cons,nil}
+use Maybe/{some,none}
+
+find <A> (cond: A -> Bool) (xs: (List A)) : (Maybe A) =
+  match xs {
+    ++: match found = (cond xs.head) {
+      true: (some xs.head)
+      false: (find cond xs.tail)
+    }: (Maybe A) // FIXME: unifier can't solve this hole
+    []: none
+  }
diff --git a/book/List/fold.kind2 b/book/List/fold.kind2
new file mode 100644
index 000000000..b576e0dd8
--- /dev/null
+++ b/book/List/fold.kind2
@@ -0,0 +1,7 @@
+use List/{cons,nil}
+
+List/fold <A> <B> (xs: (List A)) (c: A -> B -> B) (n: B) : B =
+  match xs {
+    ++: (c xs.head (List/fold xs.tail c n))
+    []: n
+  }
diff --git a/book/List/length.kind2 b/book/List/length.kind2
new file mode 100644
index 000000000..9ce24d589
--- /dev/null
+++ b/book/List/length.kind2
@@ -0,0 +1,8 @@
+use List/{cons,nil}
+use Nat/{succ,zero}
+
+length <A> (xs: (List A)) : Nat =
+  match xs {
+    ++: (succ (length xs.tail))
+    []: zero
+  }
diff --git a/book/List.map.kind2 b/book/List/map.kind2
similarity index 79%
rename from book/List.map.kind2
rename to book/List/map.kind2
index 1a1ca819e..0fcfd2873 100644
--- a/book/List.map.kind2
+++ b/book/List/map.kind2
@@ -1,12 +1,11 @@
-use List.{cons,nil}
+use List/{cons,nil}
 
 map <A> <B> (xs: (List A)) (f: A -> B) : (List B) =
   fold xs {
-    cons: (cons (f xs.head) xs.tail)
-    nil: []
+    ++: (f xs.head) ++ xs.tail
+    []: []
   }
   
-
 //map A B (xs: (List A)) (f: ∀(x: A) B) : (List B) =
   //(List.fold _ xs _ λhλt(cons _ (f h) t) [])
 
diff --git a/book/List/nil.kind2 b/book/List/nil.kind2
new file mode 100644
index 000000000..1128c0692
--- /dev/null
+++ b/book/List/nil.kind2
@@ -0,0 +1,2 @@
+nil <T> : (List T) =
+  ~λP λcons λnil nil
diff --git a/book/List/sum.kind2 b/book/List/sum.kind2
new file mode 100644
index 000000000..cab5e8072
--- /dev/null
+++ b/book/List/sum.kind2
@@ -0,0 +1,5 @@
+sum (xs: (List U60)): U60 =
+  match xs {
+    ++: (+ xs.head (sum xs.tail))
+    []: 0
+  }
diff --git a/book/Maybe.bind.kind2 b/book/Maybe.bind.kind2
deleted file mode 100644
index f15121752..000000000
--- a/book/Maybe.bind.kind2
+++ /dev/null
@@ -1,11 +0,0 @@
-Maybe.bind
-: ∀(A: *)
-  ∀(B: *)
-  ∀(a: (Maybe A))
-  ∀(b: ∀(x: A) (Maybe B))
-  (Maybe B)
-= λA λB λa λb
-  use P = λx ∀(b: ∀(x: A) (Maybe B)) (Maybe B)
-  use some = λa.value λb (b a.value)
-  use none = λb (Maybe.none B)
-  (~a P some none b)
\ No newline at end of file
diff --git a/book/Maybe.kind2 b/book/Maybe.kind2
index 9f5cd3ea2..b0278c0d6 100644
--- a/book/Maybe.kind2
+++ b/book/Maybe.kind2
@@ -1,8 +1,3 @@
-Maybe
-: ∀(T: *) *
-= λT
-  $(self: (Maybe T))
-  ∀(P: ∀(x: (Maybe T)) *)
-  ∀(some: ∀(value: T) (P (Maybe.some T value)))
-  ∀(none: (P (Maybe.none T)))
-  (P self)
\ No newline at end of file
+data Maybe T
+| some (value: T)
+| none
diff --git a/book/Maybe.monad.kind2 b/book/Maybe.monad.kind2
deleted file mode 100644
index 25faf4426..000000000
--- a/book/Maybe.monad.kind2
+++ /dev/null
@@ -1,3 +0,0 @@
-Maybe.monad
-: (Monad Maybe)
-= (Monad.new Maybe Maybe.bind Maybe.pure)
\ No newline at end of file
diff --git a/book/Maybe.none.kind2 b/book/Maybe.none.kind2
deleted file mode 100644
index 0e06f2eb4..000000000
--- a/book/Maybe.none.kind2
+++ /dev/null
@@ -1,3 +0,0 @@
-Maybe.none
-: ∀(T: *) (Maybe T)
-= λT ~λP λsome λnone none
\ No newline at end of file
diff --git a/book/Maybe.pure.kind2 b/book/Maybe.pure.kind2
deleted file mode 100644
index c40b2ac8e..000000000
--- a/book/Maybe.pure.kind2
+++ /dev/null
@@ -1,3 +0,0 @@
-Maybe.pure
-: ∀(T: *) ∀(x: T) (Maybe T)
-= Maybe.some
\ No newline at end of file
diff --git a/book/Maybe.some.kind2 b/book/Maybe.some.kind2
deleted file mode 100644
index 12be797d0..000000000
--- a/book/Maybe.some.kind2
+++ /dev/null
@@ -1,3 +0,0 @@
-Maybe.some
-: ∀(T: *) ∀(value: T) (Maybe T)
-= λT λvalue ~λP λsome λnone (some value)
\ No newline at end of file
diff --git a/book/Maybe/bind.kind2 b/book/Maybe/bind.kind2
new file mode 100644
index 000000000..731736787
--- /dev/null
+++ b/book/Maybe/bind.kind2
@@ -0,0 +1,7 @@
+use Maybe/{some,none}
+
+bind <A> <B> (a: (Maybe A)) (b: A -> (Maybe B)) : (Maybe B) =
+  match a with (b: A -> (Maybe B)) {
+    some: (b a.value)
+    none: none
+  }
diff --git a/book/Maybe/monad.kind2 b/book/Maybe/monad.kind2
new file mode 100644
index 000000000..549af5966
--- /dev/null
+++ b/book/Maybe/monad.kind2
@@ -0,0 +1,3 @@
+Maybe.monad
+: (Monad Maybe)
+= (Monad/new Maybe Maybe/bind/ Maybe/pure/)
diff --git a/book/Maybe/none.kind2 b/book/Maybe/none.kind2
new file mode 100644
index 000000000..c98c48160
--- /dev/null
+++ b/book/Maybe/none.kind2
@@ -0,0 +1,2 @@
+none <T> : (Maybe T) =
+  ~λP λsome λnone none
diff --git a/book/Maybe/pure.kind2 b/book/Maybe/pure.kind2
new file mode 100644
index 000000000..cc2aa62e4
--- /dev/null
+++ b/book/Maybe/pure.kind2
@@ -0,0 +1,2 @@
+pure <T> (x: T) : (Maybe T) =
+  (Maybe/some x)
diff --git a/book/Maybe/some.kind2 b/book/Maybe/some.kind2
new file mode 100644
index 000000000..d1901015a
--- /dev/null
+++ b/book/Maybe/some.kind2
@@ -0,0 +1,2 @@
+some <T> (value: T) : (Maybe T) =
+  ~λP λsome λnone (some value)
diff --git a/book/Monad.kind2 b/book/Monad.kind2
index e6cc7483a..4095f8fbd 100644
--- a/book/Monad.kind2
+++ b/book/Monad.kind2
@@ -9,6 +9,6 @@ Monad
       (M B)
     )
     ∀(pure: ∀(A: *) ∀(a: A) (M A))
-    (P (Monad.new M bind pure))
+    (P (Monad/new M bind pure))
   )
-  (P self)
\ No newline at end of file
+  (P self)
diff --git a/book/Monad.new.kind2 b/book/Monad/new.kind2
similarity index 95%
rename from book/Monad.new.kind2
rename to book/Monad/new.kind2
index b8f66b7d7..9380b9389 100644
--- a/book/Monad.new.kind2
+++ b/book/Monad/new.kind2
@@ -1,4 +1,4 @@
-Monad.new
+new
 : ∀(M: ∀(T: *) *)
   ∀(bind: ∀(A: *) ∀(B: *) ∀(a: (M A)) ∀(b: ∀(a: A) (M B)) (M B))
   ∀(pure: ∀(A: *) ∀(a: A) (M A))
diff --git a/book/Nat.double.kind2 b/book/Nat.double.kind2
deleted file mode 100644
index 16def3c19..000000000
--- a/book/Nat.double.kind2
+++ /dev/null
@@ -1,8 +0,0 @@
-Nat.double
-: ∀(n: Nat) Nat
-= λn
-  (~n
-    λx Nat
-    λpred (Nat.succ (Nat.succ (Nat.double pred)))
-    Nat.zero
-  )
\ No newline at end of file
diff --git a/book/Nat.equal.kind2 b/book/Nat.equal.kind2
deleted file mode 100644
index 9cd8897b3..000000000
--- a/book/Nat.equal.kind2
+++ /dev/null
@@ -1,15 +0,0 @@
-Nat.equal
-: ∀(a: Nat) ∀(b: Nat) Bool
-= λa λb
-  use P = λx ∀(b: Nat) Bool
-  use succ = λa.pred λb
-    use P = λx ∀(a.pred: Nat) Bool
-    use succ = λb.pred λa.pred (Nat.equal a.pred b.pred)
-    use zero = λa.pred Bool.false
-    (~b P succ zero a.pred)
-  use zero = λb
-    use P = λx Bool
-    use succ = λb.pred Bool.false
-    use zero = Bool.true
-    (~b P succ zero)
-  (~a P succ zero b)
\ No newline at end of file
diff --git a/book/Nat.half.kind2 b/book/Nat.half.kind2
deleted file mode 100644
index 6a3721d24..000000000
--- a/book/Nat.half.kind2
+++ /dev/null
@@ -1,8 +0,0 @@
-Nat.half
-: ∀(n: Nat) Nat
-= λn
-  (~n
-    λx Nat
-    λn (~n λx Nat λn (Nat.succ (Nat.half n)) Nat.zero)
-    Nat.zero
-  )
\ No newline at end of file
diff --git a/book/Nat.lemma.bft.kind2 b/book/Nat.lemma.bft.kind2
deleted file mode 100644
index 8e4b05ee4..000000000
--- a/book/Nat.lemma.bft.kind2
+++ /dev/null
@@ -1,7 +0,0 @@
-use Nat.{succ,zero,half,double}
-
-bft (n: Nat) : {(half (double n)) = n} =
-  match n {
-    succ: (Equal.apply _ _ _ _ succ (bft n.pred))
-    zero: {=}
-  }
diff --git a/book/Nat.succ.kind2 b/book/Nat.succ.kind2
deleted file mode 100644
index cc85fc5ce..000000000
--- a/book/Nat.succ.kind2
+++ /dev/null
@@ -1,3 +0,0 @@
-Nat.succ
-: ∀(n: Nat) Nat
-= λn ~λP λsucc λzero (succ n)
diff --git a/book/Nat.zero.kind2 b/book/Nat.zero.kind2
deleted file mode 100644
index e010e306f..000000000
--- a/book/Nat.zero.kind2
+++ /dev/null
@@ -1,3 +0,0 @@
-Nat.zero
-: Nat
-= ~λP λsucc λzero zero
\ No newline at end of file
diff --git a/book/Nat.add.kind2 b/book/Nat/add.kind2
similarity index 81%
rename from book/Nat.add.kind2
rename to book/Nat/add.kind2
index fa8a1474a..84846cc35 100644
--- a/book/Nat.add.kind2
+++ b/book/Nat/add.kind2
@@ -1,4 +1,4 @@
-use Nat.{succ,zero}
+use Nat/{succ,zero}
 
 add (a: Nat) (b: Nat) : Nat =
   match a {
diff --git a/book/Nat/double.kind2 b/book/Nat/double.kind2
new file mode 100644
index 000000000..0e9773345
--- /dev/null
+++ b/book/Nat/double.kind2
@@ -0,0 +1,7 @@
+use Nat/{succ,zero}
+
+double (n: Nat) : Nat =
+  match n {
+    succ: (succ (succ (double n.pred)))
+    zero: #0
+  }
diff --git a/book/Nat/equal.kind2 b/book/Nat/equal.kind2
new file mode 100644
index 000000000..3da619653
--- /dev/null
+++ b/book/Nat/equal.kind2
@@ -0,0 +1,32 @@
+use Nat/{succ,zero}
+use Bool/{true,false}
+
+equal (a: Nat) (b: Nat) : Bool =
+  match a with (b: Nat) {
+    succ: match b {
+      succ: (equal a.pred b.pred)
+      zero: false
+    }: Bool
+    zero: match b {
+      succ: false
+      zero: true
+    }: Bool
+  }
+
+// FIXME: the unification algorithm fails here. why?
+
+//Nat/equal
+//: ∀(a: Nat) ∀(b: Nat) Bool
+//= λa λb
+  //use a.P = _
+  //use a.succ = λa.pred λb
+    //use b.P = _
+    //use b.succ = λb.pred ?a
+    //use b.zero = Bool/false
+    //(~b b.P b.succ b.zero)
+  //use a.zero = λb
+    //use b.P = _
+    //use b.succ = λb.pred Bool/false
+    //use b.zero = Bool/true
+    //(~b b.P b.succ b.zero)
+  //({(~a a.P a.succ a.zero):∀(b: Nat) _} b)
diff --git a/book/Nat/half.kind2 b/book/Nat/half.kind2
new file mode 100644
index 000000000..0ee388f78
--- /dev/null
+++ b/book/Nat/half.kind2
@@ -0,0 +1,10 @@
+use Nat/{succ,zero}
+
+half (n: Nat) : Nat =
+  match n {
+    succ: match n.pred {
+      succ: (succ (half n.pred.pred))
+      zero: zero
+    }
+    zero: zero
+  }
diff --git a/book/Nat/lemma/bft.kind2 b/book/Nat/lemma/bft.kind2
new file mode 100644
index 000000000..c17263a68
--- /dev/null
+++ b/book/Nat/lemma/bft.kind2
@@ -0,0 +1,7 @@
+use Nat/{succ,zero,half,double}
+
+bft (n: Nat) : (half (double n)) == n =
+  match n {
+    succ: (Equal/apply succ (bft n.pred))
+    zero: {=}
+  }
diff --git a/book/Nat/succ.kind2 b/book/Nat/succ.kind2
new file mode 100644
index 000000000..183b1b2ae
--- /dev/null
+++ b/book/Nat/succ.kind2
@@ -0,0 +1,2 @@
+succ (n: Nat) : Nat =
+  ~λP λsucc λzero (succ n)
diff --git a/book/Nat/zero.kind2 b/book/Nat/zero.kind2
new file mode 100644
index 000000000..00e97a0be
--- /dev/null
+++ b/book/Nat/zero.kind2
@@ -0,0 +1,2 @@
+zero : Nat = 
+  ~λP λsucc λzero zero
diff --git a/book/Pair.fst.kind2 b/book/Pair.fst.kind2
deleted file mode 100644
index a3c017200..000000000
--- a/book/Pair.fst.kind2
+++ /dev/null
@@ -1,5 +0,0 @@
-Pair.fst
-: ∀(A: *) ∀(B: *) ∀(p: (Pair A B)) A
-= λA λB λp use P = λx A
-  use new = λa λb a
-  (~p P new)
\ No newline at end of file
diff --git a/book/Pair.get.kind2 b/book/Pair.get.kind2
deleted file mode 100644
index 46e9d386d..000000000
--- a/book/Pair.get.kind2
+++ /dev/null
@@ -1,8 +0,0 @@
-Pair.get
-: ∀(A: *)
-  ∀(B: *)
-  ∀(p: (Pair A B))
-  ∀(P: *)
-  ∀(f: ∀(a: A) ∀(b: B) P)
-  P
-= λA λB λp λP λf (~p λx P f)
\ No newline at end of file
diff --git a/book/Pair.kind2 b/book/Pair.kind2
index f90546897..7cada6910 100644
--- a/book/Pair.kind2
+++ b/book/Pair.kind2
@@ -1,9 +1,2 @@
-Pair
-: ∀(A: *) ∀(B: *) *
-= λA λB
-  $(self: (Pair A B))
-  ∀(P: ∀(pair: (Pair A B)) *)
-  ∀(new: 
-    ∀(fst: A) ∀(snd: B) (P (Pair.new A B fst snd))
-  )
-  (P self)
\ No newline at end of file
+data Pair A B
+| new (fst: A) (snd: B) : (Pair A B)
diff --git a/book/Pair.new.kind2 b/book/Pair.new.kind2
deleted file mode 100644
index 162e10ec3..000000000
--- a/book/Pair.new.kind2
+++ /dev/null
@@ -1,3 +0,0 @@
-Pair.new
-: ∀(A: *) ∀(B: *) ∀(a: A) ∀(b: B) (Pair A B)
-= λA λB λa λb ~λP λnew (new a b)
\ No newline at end of file
diff --git a/book/Pair.snd.kind2 b/book/Pair.snd.kind2
deleted file mode 100644
index 4fcf72aec..000000000
--- a/book/Pair.snd.kind2
+++ /dev/null
@@ -1,5 +0,0 @@
-Pair.snd
-: ∀(A: *) ∀(B: *) ∀(p: (Pair A B)) B
-= λA λB λp use P = λx B
-  use new = λa λb b
-  (~p P new)
\ No newline at end of file
diff --git a/book/Pair/fst.kind2 b/book/Pair/fst.kind2
new file mode 100644
index 000000000..d0bf0bdaa
--- /dev/null
+++ b/book/Pair/fst.kind2
@@ -0,0 +1,6 @@
+use Pair/{new}
+
+fst <A> <B> (p: (Pair A B)) : A =
+  match p {
+    new: p.fst
+  }
diff --git a/book/Pair/get.kind2 b/book/Pair/get.kind2
new file mode 100644
index 000000000..dfde9d7df
--- /dev/null
+++ b/book/Pair/get.kind2
@@ -0,0 +1,6 @@
+use Pair/{new}
+
+get <A> <B> <P> (p: (Pair A B)) (f: A -> B -> P) : P =
+  match p {
+    new: (f p.fst p.snd)
+  }
diff --git a/book/Pair/new.kind2 b/book/Pair/new.kind2
new file mode 100644
index 000000000..e7b647d16
--- /dev/null
+++ b/book/Pair/new.kind2
@@ -0,0 +1,2 @@
+new <A> <B> (a: A) (b: B) : (Pair A B) =
+  ~λP λnew (new a b)
diff --git a/book/Pair/snd.kind2 b/book/Pair/snd.kind2
new file mode 100644
index 000000000..293943f09
--- /dev/null
+++ b/book/Pair/snd.kind2
@@ -0,0 +1,6 @@
+use Pair/{new}
+
+snd <A> <B> (p: (Pair A B)) : B =
+  match p {
+    new: p.snd
+  }
diff --git a/book/Parser.Guard.kind2 b/book/Parser/Guard.kind2
similarity index 100%
rename from book/Parser.Guard.kind2
rename to book/Parser/Guard.kind2
diff --git a/book/Parser.Guard.get.kind2 b/book/Parser/Guard/get.kind2
similarity index 100%
rename from book/Parser.Guard.get.kind2
rename to book/Parser/Guard/get.kind2
diff --git a/book/Parser.Guard.new.kind2 b/book/Parser/Guard/new.kind2
similarity index 100%
rename from book/Parser.Guard.new.kind2
rename to book/Parser/Guard/new.kind2
diff --git a/book/Parser.Guard.pass.kind2 b/book/Parser/Guard/pass.kind2
similarity index 100%
rename from book/Parser.Guard.pass.kind2
rename to book/Parser/Guard/pass.kind2
diff --git a/book/Parser.Guard.text.kind2 b/book/Parser/Guard/text.kind2
similarity index 100%
rename from book/Parser.Guard.text.kind2
rename to book/Parser/Guard/text.kind2
diff --git a/book/Parser.Result.kind2 b/book/Parser/Result.kind2
similarity index 100%
rename from book/Parser.Result.kind2
rename to book/Parser/Result.kind2
diff --git a/book/Parser.Result.done.kind2 b/book/Parser/Result/done.kind2
similarity index 100%
rename from book/Parser.Result.done.kind2
rename to book/Parser/Result/done.kind2
diff --git a/book/Parser.Result.fail.kind2 b/book/Parser/Result/fail.kind2
similarity index 100%
rename from book/Parser.Result.fail.kind2
rename to book/Parser/Result/fail.kind2
diff --git a/book/Parser.bind.kind2 b/book/Parser/bind.kind2
similarity index 100%
rename from book/Parser.bind.kind2
rename to book/Parser/bind.kind2
diff --git a/book/Parser.char.kind2 b/book/Parser/char.kind2
similarity index 100%
rename from book/Parser.char.kind2
rename to book/Parser/char.kind2
diff --git a/book/Parser.decimal.kind2 b/book/Parser/decimal.kind2
similarity index 100%
rename from book/Parser.decimal.kind2
rename to book/Parser/decimal.kind2
diff --git a/book/Parser.fail.kind2 b/book/Parser/fail.kind2
similarity index 100%
rename from book/Parser.fail.kind2
rename to book/Parser/fail.kind2
diff --git a/book/Parser.is_eof.kind2 b/book/Parser/is_eof.kind2
similarity index 100%
rename from book/Parser.is_eof.kind2
rename to book/Parser/is_eof.kind2
diff --git a/book/Parser.map.kind2 b/book/Parser/map.kind2
similarity index 100%
rename from book/Parser.map.kind2
rename to book/Parser/map.kind2
diff --git a/book/Parser.name.kind2 b/book/Parser/name.kind2
similarity index 100%
rename from book/Parser.name.kind2
rename to book/Parser/name.kind2
diff --git a/book/Parser.oper.kind2 b/book/Parser/oper.kind2
similarity index 100%
rename from book/Parser.oper.kind2
rename to book/Parser/oper.kind2
diff --git a/book/Parser.pick.kind2 b/book/Parser/pick.kind2
similarity index 100%
rename from book/Parser.pick.kind2
rename to book/Parser/pick.kind2
diff --git a/book/Parser.pick_while.kind2 b/book/Parser/pick_while.kind2
similarity index 100%
rename from book/Parser.pick_while.kind2
rename to book/Parser/pick_while.kind2
diff --git a/book/Parser.pick_while.go.kind2 b/book/Parser/pick_while/go.kind2
similarity index 100%
rename from book/Parser.pick_while.go.kind2
rename to book/Parser/pick_while/go.kind2
diff --git a/book/Parser.pure.kind2 b/book/Parser/pure.kind2
similarity index 100%
rename from book/Parser.pure.kind2
rename to book/Parser/pure.kind2
diff --git a/book/Parser.repeat.kind2 b/book/Parser/repeat.kind2
similarity index 100%
rename from book/Parser.repeat.kind2
rename to book/Parser/repeat.kind2
diff --git a/book/Parser.skip.kind2 b/book/Parser/skip.kind2
similarity index 100%
rename from book/Parser.skip.kind2
rename to book/Parser/skip.kind2
diff --git a/book/Parser.take.kind2 b/book/Parser/take.kind2
similarity index 100%
rename from book/Parser.take.kind2
rename to book/Parser/take.kind2
diff --git a/book/Parser.test.kind2 b/book/Parser/test.kind2
similarity index 100%
rename from book/Parser.test.kind2
rename to book/Parser/test.kind2
diff --git a/book/Parser.text.kind2 b/book/Parser/text.kind2
similarity index 100%
rename from book/Parser.text.kind2
rename to book/Parser/text.kind2
diff --git a/book/Parser.until.kind2 b/book/Parser/until.kind2
similarity index 76%
rename from book/Parser.until.kind2
rename to book/Parser/until.kind2
index 465b82e70..de801b248 100644
--- a/book/Parser.until.kind2
+++ b/book/Parser/until.kind2
@@ -5,8 +5,8 @@ Parser.until
   (Parser (List A))
 = λA λuntil λparse
   (Parser.map
-    (List.Concatenator A)
+    (List.Chunk A)
     (List A)
-    (List.Concatenator.build A)
+    (List.Chunk.build A)
     (Parser.until.go A until parse λx x)
   )
\ No newline at end of file
diff --git a/book/Parser.until.go.kind2 b/book/Parser/until/go.kind2
similarity index 51%
rename from book/Parser.until.go.kind2
rename to book/Parser/until/go.kind2
index fc2fd877a..6eab0dc9f 100644
--- a/book/Parser.until.go.kind2
+++ b/book/Parser/until/go.kind2
@@ -2,17 +2,17 @@ Parser.until.go
 : ∀(A: *)
   ∀(until: (Parser Bool))
   ∀(parse: (Parser A))
-  ∀(terms: (List.Concatenator A))
-  (Parser (List.Concatenator A))
+  ∀(terms: (List.Chunk A))
+  (Parser (List.Chunk A))
 = λA λuntil λparse λterms λcode
-  use P = λx (Parser.Result (List.Concatenator A))
+  use P = λx (Parser.Result (List.Chunk A))
   use done = λcode λstop
     use P = λx
-      ∀(code: String) (Parser.Result (List.Concatenator A))
+      ∀(code: String) (Parser.Result (List.Chunk A))
     use true = λcode
-      (Parser.Result.done (List.Concatenator A) code terms)
+      (Parser.Result.done (List.Chunk A) code terms)
     use false = λcode
-      use P = λx (Parser.Result (List.Concatenator A))
+      use P = λx (Parser.Result (List.Chunk A))
       use done = λcode λvalue
         (Parser.until.go
           A
@@ -21,8 +21,8 @@ Parser.until.go
           λx (terms (List.cons A value x))
           code
         )
-      use fail = λerror (Parser.Result.fail (List.Concatenator A) error)
+      use fail = λerror (Parser.Result.fail (List.Chunk A) error)
       (~(parse code) P done fail)
     (~stop P true false code)
-  use fail = λerror (Parser.Result.fail (List.Concatenator A) error)
+  use fail = λerror (Parser.Result.fail (List.Chunk A) error)
   (~(until code) P done fail)
\ No newline at end of file
diff --git a/book/Parser.variant.kind2 b/book/Parser/variant.kind2
similarity index 100%
rename from book/Parser.variant.kind2
rename to book/Parser/variant.kind2
diff --git a/book/QBool.false.kind2 b/book/QBool/false.kind2
similarity index 100%
rename from book/QBool.false.kind2
rename to book/QBool/false.kind2
diff --git a/book/QBool.match.kind2 b/book/QBool/match.kind2
similarity index 100%
rename from book/QBool.match.kind2
rename to book/QBool/match.kind2
diff --git a/book/QBool.true.kind2 b/book/QBool/true.kind2
similarity index 100%
rename from book/QBool.true.kind2
rename to book/QBool/true.kind2
diff --git a/book/QBool2.false.kind2 b/book/QBool2/false.kind2
similarity index 100%
rename from book/QBool2.false.kind2
rename to book/QBool2/false.kind2
diff --git a/book/QBool2.match.kind2 b/book/QBool2/match.kind2
similarity index 100%
rename from book/QBool2.match.kind2
rename to book/QBool2/match.kind2
diff --git a/book/QBool2.true.kind2 b/book/QBool2/true.kind2
similarity index 100%
rename from book/QBool2.true.kind2
rename to book/QBool2/true.kind2
diff --git a/book/Sigma.new.kind2 b/book/Sigma/new.kind2
similarity index 100%
rename from book/Sigma.new.kind2
rename to book/Sigma/new.kind2
diff --git a/book/String.Concatenator.build.kind2 b/book/String.Concatenator.build.kind2
deleted file mode 100644
index 7d27664d5..000000000
--- a/book/String.Concatenator.build.kind2
+++ /dev/null
@@ -1,3 +0,0 @@
-String.Concatenator.build
-: ∀(x: String.Concatenator) String
-= (List.Concatenator.build Char)
\ No newline at end of file
diff --git a/book/String.Concatenator.concat.kind2 b/book/String.Concatenator.concat.kind2
deleted file mode 100644
index 3985eada8..000000000
--- a/book/String.Concatenator.concat.kind2
+++ /dev/null
@@ -1,4 +0,0 @@
-String.Concatenator.concat
-: ∀(xs: String.Concatenator) ∀(ys: String.Concatenator)
-  String.Concatenator
-= (List.Concatenator.concat Char)
\ No newline at end of file
diff --git a/book/String.Concatenator.from_string.kind2 b/book/String.Concatenator.from_string.kind2
deleted file mode 100644
index c4cfb210c..000000000
--- a/book/String.Concatenator.from_string.kind2
+++ /dev/null
@@ -1,3 +0,0 @@
-String.Concatenator.from_string
-: ∀(xs: String) String.Concatenator
-= (List.Concatenator.from_list Char)
\ No newline at end of file
diff --git a/book/String.Concatenator.join.kind2 b/book/String.Concatenator.join.kind2
deleted file mode 100644
index 8a9c26a49..000000000
--- a/book/String.Concatenator.join.kind2
+++ /dev/null
@@ -1,3 +0,0 @@
-String.Concatenator.join
-: ∀(xs: (List String.Concatenator)) String.Concatenator
-= (List.Concatenator.join Char)
\ No newline at end of file
diff --git a/book/String.Concatenator.kind2 b/book/String.Concatenator.kind2
deleted file mode 100644
index 694122de0..000000000
--- a/book/String.Concatenator.kind2
+++ /dev/null
@@ -1,3 +0,0 @@
-String.Concatenator
-: *
-= (List.Concatenator Char)
\ No newline at end of file
diff --git a/book/String.Map.kind2 b/book/String.Map.kind2
deleted file mode 100644
index 3f29c03fb..000000000
--- a/book/String.Map.kind2
+++ /dev/null
@@ -1,3 +0,0 @@
-String.Map
-: ∀(V: *) *
-= λV (BBT String V)
\ No newline at end of file
diff --git a/book/String.begin.kind2 b/book/String.begin.kind2
deleted file mode 100644
index 852663e39..000000000
--- a/book/String.begin.kind2
+++ /dev/null
@@ -1,3 +0,0 @@
-String.begin
-: ∀(str: String) String
-= λstr (List.begin Char str)
\ No newline at end of file
diff --git a/book/String.concat.kind2 b/book/String.concat.kind2
deleted file mode 100644
index ca57b8231..000000000
--- a/book/String.concat.kind2
+++ /dev/null
@@ -1,3 +0,0 @@
-String.concat
-: ∀(xs: String) ∀(ys: String) String
-= (List.concat Char)
\ No newline at end of file
diff --git a/book/String.cons.kind2 b/book/String.cons.kind2
deleted file mode 100644
index 4cdf4eb5b..000000000
--- a/book/String.cons.kind2
+++ /dev/null
@@ -1,3 +0,0 @@
-String.cons
-: ∀(head: Char) ∀(tail: String) String
-= λhead λtail ~λP λcons λnil (cons head tail)
\ No newline at end of file
diff --git a/book/String.indent.kind2 b/book/String.indent.kind2
deleted file mode 100644
index 641398be2..000000000
--- a/book/String.indent.kind2
+++ /dev/null
@@ -1,11 +0,0 @@
-String.indent
-: ∀(tab: Nat) String
-= λtab
-  use P = λx String
-  use succ = λtab.pred
-    (String.cons
-      32
-      (String.cons 32 (String.indent tab.pred))
-    )
-  use zero = String.nil
-  (~tab P succ zero)
\ No newline at end of file
diff --git a/book/String.join.kind2 b/book/String.join.kind2
deleted file mode 100644
index a5ad501c4..000000000
--- a/book/String.join.kind2
+++ /dev/null
@@ -1,7 +0,0 @@
-String.join
-: ∀(sep: String) ∀(strs: (List String)) String
-= λsep λstrs
-  use P = λx String
-  use cons = λh λt (String.concat h (String.join.go sep t))
-  use nil = String.nil
-  (~strs P cons nil)
\ No newline at end of file
diff --git a/book/String.kind2 b/book/String.kind2
index 9d355e260..0c6c09d03 100644
--- a/book/String.kind2
+++ b/book/String.kind2
@@ -1,3 +1,2 @@
-String
-: *
-= (List Char)
+String : * =
+  (List Char)
diff --git a/book/String.length.kind2 b/book/String.length.kind2
deleted file mode 100644
index 7dc5553d5..000000000
--- a/book/String.length.kind2
+++ /dev/null
@@ -1,3 +0,0 @@
-String.length
-: ∀(a: String) Nat
-= λa (List.length Char a)
diff --git a/book/String.newline.kind2 b/book/String.newline.kind2
deleted file mode 100644
index a8ad5d876..000000000
--- a/book/String.newline.kind2
+++ /dev/null
@@ -1,3 +0,0 @@
-String.newline
-: String
-= (String.cons 10 String.nil)
\ No newline at end of file
diff --git a/book/String.nil.kind2 b/book/String.nil.kind2
deleted file mode 100644
index a06865d12..000000000
--- a/book/String.nil.kind2
+++ /dev/null
@@ -1,3 +0,0 @@
-String.nil
-: String
-= ~λP λcons λnil nil
\ No newline at end of file
diff --git a/book/String.skip.comment.kind2 b/book/String.skip.comment.kind2
deleted file mode 100644
index 4b4327ed4..000000000
--- a/book/String.skip.comment.kind2
+++ /dev/null
@@ -1,11 +0,0 @@
-String.skip.comment
-: ∀(str: String) String
-= λstr
-  use P = λx String
-  use cons = λc0 λcs
-    use P = λx ∀(c0: Char) ∀(cs: String) String
-    use true = λc0 λcs (String.skip cs)
-    use false = λc0 λcs (String.skip.comment cs)
-    (~(Char.is_newline c0) P true false c0 cs)
-  use nil = String.nil
-  (~str P cons nil)
\ No newline at end of file
diff --git a/book/String.skip.kind2 b/book/String.skip.kind2
deleted file mode 100644
index d20ba2188..000000000
--- a/book/String.skip.kind2
+++ /dev/null
@@ -1,23 +0,0 @@
-String.skip
-: ∀(str: String) String
-= λstr
-  use P = λx String
-  use cons = λc0 λcs
-    use P = λx ∀(c0: Char) ∀(cs: String) String
-    use true = λc0 λcs (String.skip cs)
-    use false = λc0 λcs
-      use P = λx ∀(c0: Char) ∀(cs: String) String
-      use true = λc0 λcs
-        use P = λx ∀(c0: Char) String
-        use cons = λc1 λcs λc0
-          use P = λx ∀(c0: Char) ∀(c1: Char) ∀(cs: String) String
-          use true = λc0 λc1 λcs (String.skip.comment cs)
-          use false = λc0 λc1 λcs (String.cons c0 (String.cons c1 cs))
-          (~(Char.is_slash c1) P true false c0 c1 cs)
-        use nil = λc0 (String.cons c0 String.nil)
-        (~cs P cons nil c0)
-      use false = λc0 λcs (String.cons c0 cs)
-      (~(Char.is_slash c0) P true false c0 cs)
-    (~(Char.is_blank c0) P true false c0 cs)
-  use nil = String.nil
-  (~str P cons nil)
\ No newline at end of file
diff --git a/book/String.unpar.kind2 b/book/String.unpar.kind2
deleted file mode 100644
index 3134fe72e..000000000
--- a/book/String.unpar.kind2
+++ /dev/null
@@ -1,11 +0,0 @@
-String.unpar
-: ∀(fst: Char) ∀(lst: Char) ∀(str: String) String
-= λfst λlst λstr
-  use P = λx String
-  use cons = λhead λtail
-    use P = λx ∀(head: Char) ∀(tail: String) String
-    use true = λhead λtail (String.begin tail)
-    use false = λhead λtail (String.cons head tail)
-    (~(Char.equal head fst) P true false head tail)
-  use nil = String.nil
-  (~str P cons nil)
\ No newline at end of file
diff --git a/book/String.wrap.go.kind2 b/book/String.wrap.go.kind2
deleted file mode 100644
index adc9dd4fb..000000000
--- a/book/String.wrap.go.kind2
+++ /dev/null
@@ -1,7 +0,0 @@
-String.wrap.go
-: ∀(str: String) ∀(end: String) String
-= λstr λend
-  use P = λx ∀(end: String) String
-  use cons = λh λt λend (String.cons h (String.wrap.go t end))
-  use nil = λend (String.concat end String.nil)
-  (~str P cons nil end)
\ No newline at end of file
diff --git a/book/String.wrap.kind2 b/book/String.wrap.kind2
deleted file mode 100644
index c557a601d..000000000
--- a/book/String.wrap.kind2
+++ /dev/null
@@ -1,4 +0,0 @@
-String.wrap
-: ∀(ini: String) ∀(str: String) ∀(end: String) String
-= λini λstr λend
-  (String.concat ini (String.wrap.go str end))
\ No newline at end of file
diff --git a/book/String/Chunk.kind2 b/book/String/Chunk.kind2
new file mode 100644
index 000000000..4322c16d6
--- /dev/null
+++ b/book/String/Chunk.kind2
@@ -0,0 +1,2 @@
+Chunk : * =
+  (List/Chunk Char)
diff --git a/book/String/Chunk/build.kind2 b/book/String/Chunk/build.kind2
new file mode 100644
index 000000000..3d355c61b
--- /dev/null
+++ b/book/String/Chunk/build.kind2
@@ -0,0 +1,3 @@
+String.Chunk.build
+: ∀(x: String.Chunk) String
+= (List.Chunk.build Char)
\ No newline at end of file
diff --git a/book/String/Chunk/concat.kind2 b/book/String/Chunk/concat.kind2
new file mode 100644
index 000000000..1ab80a6d3
--- /dev/null
+++ b/book/String/Chunk/concat.kind2
@@ -0,0 +1,4 @@
+String.Chunk.concat
+: ∀(xs: String.Chunk) ∀(ys: String.Chunk)
+  String.Chunk
+= (List.Chunk.concat Char)
\ No newline at end of file
diff --git a/book/String/Chunk/from_string.kind2 b/book/String/Chunk/from_string.kind2
new file mode 100644
index 000000000..2f3fc2c2d
--- /dev/null
+++ b/book/String/Chunk/from_string.kind2
@@ -0,0 +1,3 @@
+String.Chunk.from_string
+: ∀(xs: String) String.Chunk
+= (List.Chunk.from_list Char)
\ No newline at end of file
diff --git a/book/String/Chunk/join.kind2 b/book/String/Chunk/join.kind2
new file mode 100644
index 000000000..4fafce5d6
--- /dev/null
+++ b/book/String/Chunk/join.kind2
@@ -0,0 +1,3 @@
+String.Chunk.join
+: ∀(xs: (List String.Chunk)) String.Chunk
+= (List.Chunk.join Char)
\ No newline at end of file
diff --git a/book/String/Map.kind2 b/book/String/Map.kind2
new file mode 100644
index 000000000..63572a1e0
--- /dev/null
+++ b/book/String/Map.kind2
@@ -0,0 +1,3 @@
+Map
+: ∀(V: *) *
+= λV (BBT String V)
diff --git a/book/String.Map.from_list.kind2 b/book/String/Map/from_list.kind2
similarity index 100%
rename from book/String.Map.from_list.kind2
rename to book/String/Map/from_list.kind2
diff --git a/book/String.Map.get.kind2 b/book/String/Map/get.kind2
similarity index 100%
rename from book/String.Map.get.kind2
rename to book/String/Map/get.kind2
diff --git a/book/String.Map.got.kind2 b/book/String/Map/got.kind2
similarity index 100%
rename from book/String.Map.got.kind2
rename to book/String/Map/got.kind2
diff --git a/book/String.Map.has.kind2 b/book/String/Map/has.kind2
similarity index 100%
rename from book/String.Map.has.kind2
rename to book/String/Map/has.kind2
diff --git a/book/String.Map.has.linear.kind2 b/book/String/Map/has/linear.kind2
similarity index 100%
rename from book/String.Map.has.linear.kind2
rename to book/String/Map/has/linear.kind2
diff --git a/book/String.Map.new.kind2 b/book/String/Map/new.kind2
similarity index 100%
rename from book/String.Map.new.kind2
rename to book/String/Map/new.kind2
diff --git a/book/String.Map.set.kind2 b/book/String/Map/set.kind2
similarity index 100%
rename from book/String.Map.set.kind2
rename to book/String/Map/set.kind2
diff --git a/book/String.Map.to_list.kind2 b/book/String/Map/to_list.kind2
similarity index 100%
rename from book/String.Map.to_list.kind2
rename to book/String/Map/to_list.kind2
diff --git a/book/String/begin.kind2 b/book/String/begin.kind2
new file mode 100644
index 000000000..39a0120d3
--- /dev/null
+++ b/book/String/begin.kind2
@@ -0,0 +1,2 @@
+begin (str: String) : String =
+  (List/begin str)
diff --git a/book/String.cmp.kind2 b/book/String/cmp.kind2
similarity index 55%
rename from book/String.cmp.kind2
rename to book/String/cmp.kind2
index 13d33d392..daf041ff8 100644
--- a/book/String.cmp.kind2
+++ b/book/String/cmp.kind2
@@ -1,4 +1,4 @@
-String.cmp
+String/cmp
 : ∀(a: String) ∀(b: String) Cmp
 = λa λb
   use P = λx ∀(b: String) Cmp
@@ -6,15 +6,15 @@ String.cmp
     use P = λx ∀(a.head: Char) ∀(a.tail: String) Cmp
     use cons = λb.head λb.tail λa.head λa.tail
       use P = λx Cmp
-      use ltn = Cmp.ltn
-      use eql = (String.cmp a.tail b.tail)
-      use gtn = Cmp.gtn
-      (~(U60.cmp a.head b.head) P ltn eql gtn)
-    use nil = λa.head λa.tail Cmp.gtn
+      use ltn = Cmp/ltn
+      use eql = (cmp a.tail b.tail)
+      use gtn = Cmp/gtn
+      (~(U60/cmp a.head b.head) P ltn eql gtn)
+    use nil = λa.head λa.tail Cmp/gtn
     (~b P cons nil a.head a.tail)
   use nil = λb
     use P = λx Cmp
-    use cons = λb.head λb.tail Cmp.ltn
-    use nil = Cmp.eql
+    use cons = λb.head λb.tail Cmp/ltn
+    use nil = Cmp/eql
     (~b P cons nil)
-  (~a P cons nil b)
\ No newline at end of file
+  (~a P cons nil b)
diff --git a/book/String/concat.kind2 b/book/String/concat.kind2
new file mode 100644
index 000000000..404527f3e
--- /dev/null
+++ b/book/String/concat.kind2
@@ -0,0 +1,2 @@
+concat (xs: String) (ys: String) : String =
+  (List/concat xs ys)
diff --git a/book/String/cons.kind2 b/book/String/cons.kind2
new file mode 100644
index 000000000..3b1da2bfe
--- /dev/null
+++ b/book/String/cons.kind2
@@ -0,0 +1,2 @@
+String.cons (head: Char) (tail: String) : String =
+  ~λP λcons λnil (cons head tail)
diff --git a/book/String.equal.kind2 b/book/String/equal.kind2
similarity index 50%
rename from book/String.equal.kind2
rename to book/String/equal.kind2
index f1f074586..7f5ddaf84 100644
--- a/book/String.equal.kind2
+++ b/book/String/equal.kind2
@@ -1,19 +1,17 @@
-String.equal
-: ∀(a: String) ∀(b: String) Bool
-= λa λb
+String/equal (a: String) (b: String) : Bool =
   use P = λx ∀(b: String) Bool
   use cons = λa.head λa.tail λb
     use P = λx ∀(a.head: Char) ∀(a.tail: String) Bool
     use cons = λb.head λb.tail λa.head λa.tail
-      (Bool.and
-        (U60.equal a.head b.head)
-        (String.equal a.tail b.tail)
+      (Bool/and
+        (U60/equal a.head b.head)
+        (String/equal a.tail b.tail)
       )
-    use nil = λa.head λa.tail Bool.false
+    use nil = λa.head λa.tail Bool/false
     (~b P cons nil a.head a.tail)
   use nil = λb
     use P = λx Bool
-    use cons = λb.head λb.tail Bool.false
-    use nil = Bool.true
+    use cons = λb.head λb.tail Bool/false
+    use nil = Bool/true
     (~b P cons nil)
-  (~a P cons nil b)
\ No newline at end of file
+  (~a P cons nil b)
diff --git a/book/String/indent.kind2 b/book/String/indent.kind2
new file mode 100644
index 000000000..f7f39e7fc
--- /dev/null
+++ b/book/String/indent.kind2
@@ -0,0 +1,7 @@
+indent
+: ∀(tab: Nat) String
+= λtab
+  use P    = λx String
+  use succ = λtab.pred (String/cons 32 (String/cons 32 (indent tab.pred)))
+  use zero = String/nil
+  (~tab P succ zero)
diff --git a/book/String/join.kind2 b/book/String/join.kind2
new file mode 100644
index 000000000..9869091b7
--- /dev/null
+++ b/book/String/join.kind2
@@ -0,0 +1,7 @@
+join
+: ∀(sep: String) ∀(strs: (List String)) String
+= λsep λstrs
+  use P = λx String
+  use cons = λh λt (String/concat h (String/join/go sep t))
+  use nil = String/nil
+  (~strs P cons nil)
diff --git a/book/String.join.go.kind2 b/book/String/join/go.kind2
similarity index 50%
rename from book/String.join.go.kind2
rename to book/String/join/go.kind2
index f3cf20307..541c7640c 100644
--- a/book/String.join.go.kind2
+++ b/book/String/join/go.kind2
@@ -1,11 +1,11 @@
-String.join.go
+go
 : ∀(sep: String) ∀(strs: (List String)) String
 = λsep λstrs
   use P = λx String
   use cons = λh λt
-    (String.concat
+    (String/concat
       sep
-      (String.concat h (String.join.go sep t))
+      (String/concat h (go sep t))
     )
-  use nil = String.nil
-  (~strs P cons nil)
\ No newline at end of file
+  use nil = String/nil
+  (~strs P cons nil)
diff --git a/book/String/length.kind2 b/book/String/length.kind2
new file mode 100644
index 000000000..c40efc47e
--- /dev/null
+++ b/book/String/length.kind2
@@ -0,0 +1,3 @@
+String/length
+: ∀(a: String) Nat
+= λa (List/length a)
diff --git a/book/String/newline.kind2 b/book/String/newline.kind2
new file mode 100644
index 000000000..bdeb1b9cd
--- /dev/null
+++ b/book/String/newline.kind2
@@ -0,0 +1,3 @@
+newline
+: String
+= (String/cons 10 String/nil)
diff --git a/book/String/nil.kind2 b/book/String/nil.kind2
new file mode 100644
index 000000000..5d4cd470e
--- /dev/null
+++ b/book/String/nil.kind2
@@ -0,0 +1,2 @@
+String.nil : String =
+  ~λP λcons λnil nil
diff --git a/book/String.quote.kind2 b/book/String/quote.kind2
similarity index 100%
rename from book/String.quote.kind2
rename to book/String/quote.kind2
diff --git a/book/String/skip.kind2 b/book/String/skip.kind2
new file mode 100644
index 000000000..b97124cea
--- /dev/null
+++ b/book/String/skip.kind2
@@ -0,0 +1,23 @@
+skip
+: ∀(str: String) String
+= λstr
+  use P = λx String
+  use cons = λc0 λcs
+    use P = λx ∀(c0: Char) ∀(cs: String) String
+    use true = λc0 λcs (String/skip cs)
+    use false = λc0 λcs
+      use P = λx ∀(c0: Char) ∀(cs: String) String
+      use true = λc0 λcs
+        use P = λx ∀(c0: Char) String
+        use cons = λc1 λcs λc0
+          use P = λx ∀(c0: Char) ∀(c1: Char) ∀(cs: String) String
+          use true = λc0 λc1 λcs (String/skip/comment cs)
+          use false = λc0 λc1 λcs (String/cons c0 (String/cons c1 cs))
+          (~(Char/is_slash c1) P true false c0 c1 cs)
+        use nil = λc0 (String/cons c0 String/nil)
+        (~cs P cons nil c0)
+      use false = λc0 λcs (String/cons c0 cs)
+      (~(Char/is_slash c0) P true false c0 cs)
+    (~(Char/is_blank c0) P true false c0 cs)
+  use nil = String/nil
+  (~str P cons nil)
diff --git a/book/String/skip/comment.kind2 b/book/String/skip/comment.kind2
new file mode 100644
index 000000000..c08a052be
--- /dev/null
+++ b/book/String/skip/comment.kind2
@@ -0,0 +1,11 @@
+comment
+: ∀(str: String) String
+= λstr
+  use P = λx String
+  use cons = λc0 λcs
+    use P = λx ∀(c0: Char) ∀(cs: String) String
+    use true = λc0 λcs (String/skip cs)
+    use false = λc0 λcs (String/skip/comment cs)
+    (~(Char/is_newline c0) P true false c0 cs)
+  use nil = String/nil
+  (~str P cons nil)
diff --git a/book/String/unpar.kind2 b/book/String/unpar.kind2
new file mode 100644
index 000000000..5324d6812
--- /dev/null
+++ b/book/String/unpar.kind2
@@ -0,0 +1,11 @@
+unpar
+: ∀(fst: Char) ∀(lst: Char) ∀(str: String) String
+= λfst λlst λstr
+  use P = λx String
+  use cons = λhead λtail
+    use P = λx ∀(head: Char) ∀(tail: String) String
+    use true = λhead λtail (String/begin tail)
+    use false = λhead λtail (String/cons head tail)
+    (~(Char/equal head fst) P true false head tail)
+  use nil = String/nil
+  (~str P cons nil)
diff --git a/book/String/wrap.kind2 b/book/String/wrap.kind2
new file mode 100644
index 000000000..5c364185e
--- /dev/null
+++ b/book/String/wrap.kind2
@@ -0,0 +1,2 @@
+wrap (ini: String) (str: String) (end: String) : String =
+  (String/concat ini (String/wrap/go str end))
diff --git a/book/String/wrap/go.kind2 b/book/String/wrap/go.kind2
new file mode 100644
index 000000000..5888c09da
--- /dev/null
+++ b/book/String/wrap/go.kind2
@@ -0,0 +1,7 @@
+go
+: ∀(str: String) ∀(end: String) String
+= λstr λend
+  use P = λx ∀(end: String) String
+  use cons = λh λt λend (String/cons h (String/wrap/go t end))
+  use nil = λend (String/concat end String/nil)
+  (~str P cons nil end)
diff --git a/book/The.kind2 b/book/The.kind2
index 41e47d2b8..ffe1b4b10 100644
--- a/book/The.kind2
+++ b/book/The.kind2
@@ -1,9 +1,2 @@
-The
-: ∀(A: *)
-  ∀(x: A)
-  *
-= λA λx
-  $(self: (The A x))
-  ∀(P: ∀(x: A) ∀(p: (The A x)) *)
-  ∀(value: ∀(x: A) (P x (The.value A x)))
-  (P x self)
+data The A (x: A)
+| value (x: A) : (The A x)
diff --git a/book/The.value.kind2 b/book/The.value.kind2
deleted file mode 100644
index 97d3bb55a..000000000
--- a/book/The.value.kind2
+++ /dev/null
@@ -1,7 +0,0 @@
-The.value
-: ∀(A: *)
-  ∀(x: A)
-  (The A x)
-= λA λx
-  ~λP λvalue (value x) 
-
diff --git a/book/The/value.kind2 b/book/The/value.kind2
new file mode 100644
index 000000000..68df4493d
--- /dev/null
+++ b/book/The/value.kind2
@@ -0,0 +1,2 @@
+value <A> (x: A) : (The A x) =
+  ~λP λvalue (value x)
diff --git a/book/U60.Map.kind2 b/book/U60.Map.kind2
deleted file mode 100644
index a8b8b1944..000000000
--- a/book/U60.Map.kind2
+++ /dev/null
@@ -1,3 +0,0 @@
-U60.Map
-: ∀(V: *) *
-= λV (BBT U60 V)
\ No newline at end of file
diff --git a/book/U60.abs_diff.kind2 b/book/U60.abs_diff.kind2
deleted file mode 100644
index c0ee027bd..000000000
--- a/book/U60.abs_diff.kind2
+++ /dev/null
@@ -1,7 +0,0 @@
-U60.abs_diff
-: ∀(a: U60) ∀(b: U60) U60
-= λa λb
-  use P = λx U60
-  use true = (- b a)
-  use false = (- a b)
-  (~(U60.to_bool (< a b)) P true false)
diff --git a/book/U60.cmp.kind2 b/book/U60.cmp.kind2
deleted file mode 100644
index ef74da622..000000000
--- a/book/U60.cmp.kind2
+++ /dev/null
@@ -1,9 +0,0 @@
-U60.cmp
-: ∀(a: U60) ∀(b: U60) Cmp
-= λa λb
-  (U60.if
-    (== a b)
-    Cmp
-    (U60.if (< a b) Cmp Cmp.gtn Cmp.ltn)
-    Cmp.eql
-  )
diff --git a/book/U60.equal.kind2 b/book/U60.equal.kind2
deleted file mode 100644
index 5108af028..000000000
--- a/book/U60.equal.kind2
+++ /dev/null
@@ -1,7 +0,0 @@
-U60.equal
-: ∀(a: U60) ∀(b: U60) Bool
-= λa λb
-  switch x = (== a b) {
-    0: Bool.false
-    _: Bool.true 
-  }: Bool
diff --git a/book/U60.from_nat.kind2 b/book/U60.from_nat.kind2
deleted file mode 100644
index df4809322..000000000
--- a/book/U60.from_nat.kind2
+++ /dev/null
@@ -1,7 +0,0 @@
-U60.from_nat
-: ∀(n: Nat) U60
-= λn
-  use P = λx U60
-  use succ = λn.pred (+ 1 (U60.from_nat n.pred))
-  use zero = 0
-  (~n P succ zero)
diff --git a/book/U60.if.kind2 b/book/U60.if.kind2
deleted file mode 100644
index 96f8fdda0..000000000
--- a/book/U60.if.kind2
+++ /dev/null
@@ -1,3 +0,0 @@
-U60.if
-: ∀(x: U60) ∀(P: *) ∀(t: P) ∀(f: P) P
-= λx λP λt λf switch x = x { 0: t _: f }: P
\ No newline at end of file
diff --git a/book/U60.match.kind2 b/book/U60.match.kind2
deleted file mode 100644
index 50f55e3a0..000000000
--- a/book/U60.match.kind2
+++ /dev/null
@@ -1,8 +0,0 @@
-U60.switch
-: ∀(x: U60)
-  ∀(P: ∀(x: U60) *)
-  ∀(s: ∀(x: U60) (P (+ 1 x)))
-  ∀(z: (P 0))
-  (P x)
-= λx λP λs λz
-  switch self = x { 0: z _: (s self-1) }: (P self)
\ No newline at end of file
diff --git a/book/U60.max.kind2 b/book/U60.max.kind2
deleted file mode 100644
index 75a4b5c17..000000000
--- a/book/U60.max.kind2
+++ /dev/null
@@ -1,3 +0,0 @@
-U60.max
-: ∀(a: U60) ∀(b: U60) U60
-= λa λb (~(U60.to_bool (> a b)) λx U60 a b)
diff --git a/book/U60.min.kind2 b/book/U60.min.kind2
deleted file mode 100644
index 2e11901f7..000000000
--- a/book/U60.min.kind2
+++ /dev/null
@@ -1,3 +0,0 @@
-U60.min
-: ∀(a: U60) ∀(b: U60) U60
-= λa λb (~(U60.to_bool (< a b)) λx U60 a b)
diff --git a/book/U60.name.kind2 b/book/U60.name.kind2
deleted file mode 100644
index b8cbce23e..000000000
--- a/book/U60.name.kind2
+++ /dev/null
@@ -1,3 +0,0 @@
-U60.name
-: ∀(n: U60) String
-= λn (String.Concatenator.build (U60.name.go (+ n 1)))
\ No newline at end of file
diff --git a/book/U60.show.go.kind2 b/book/U60.show.go.kind2
deleted file mode 100644
index d56df1cf9..000000000
--- a/book/U60.show.go.kind2
+++ /dev/null
@@ -1,11 +0,0 @@
-U60.show.go
-: ∀(n: U60) String.Concatenator
-= λn
-  switch x = (< n 10) {
-    0: λnil
-    (U60.show.go
-      (/ n 10)
-      (String.cons (+ 48 (% n 10)) nil)
-    )
-    _: λnil (String.cons (+ 48 n) nil) 
-  }: String.Concatenator
\ No newline at end of file
diff --git a/book/U60.show.kind2 b/book/U60.show.kind2
deleted file mode 100644
index b7d05d526..000000000
--- a/book/U60.show.kind2
+++ /dev/null
@@ -1,3 +0,0 @@
-U60.show
-: ∀(n: U60) String
-= λn (String.Concatenator.build (U60.show.go n))
\ No newline at end of file
diff --git a/book/U60.to_bool.kind2 b/book/U60.to_bool.kind2
deleted file mode 100644
index cceebad2a..000000000
--- a/book/U60.to_bool.kind2
+++ /dev/null
@@ -1,5 +0,0 @@
-U60.to_bool (x: U60) : Bool =
-  switch x {
-    0: Bool.false
-    _: Bool.true
-  }: Bool
diff --git a/book/U60/Map.kind2 b/book/U60/Map.kind2
new file mode 100644
index 000000000..bd7b1bb4d
--- /dev/null
+++ b/book/U60/Map.kind2
@@ -0,0 +1,2 @@
+Map (V: *) : * =
+  (BBT U60 V)
diff --git a/book/U60/abs_diff.kind2 b/book/U60/abs_diff.kind2
new file mode 100644
index 000000000..87b9dd757
--- /dev/null
+++ b/book/U60/abs_diff.kind2
@@ -0,0 +1,7 @@
+use Bool/{true,false}
+
+abs_diff (a: U60) (b: U60) : U60 =
+  match x = (U60/to_bool (< a b)) {
+    true: (- b a)
+    false: (- a b)
+  }: U60 // FIXME: unifier can't fill this type
diff --git a/book/U60/cmp.kind2 b/book/U60/cmp.kind2
new file mode 100644
index 000000000..c912210a1
--- /dev/null
+++ b/book/U60/cmp.kind2
@@ -0,0 +1,4 @@
+cmp (a: U60) (b: U60) : Cmp =
+  (U60/if (== a b)
+    (U60/if (< a b) Cmp/gtn Cmp/ltn)
+    Cmp/eql)
diff --git a/book/U60/equal.kind2 b/book/U60/equal.kind2
new file mode 100644
index 000000000..9939e705f
--- /dev/null
+++ b/book/U60/equal.kind2
@@ -0,0 +1,7 @@
+use Bool/{true,false}
+
+equal (a: U60) (b: U60) : Bool =
+  switch x = (== a b) {
+    0: false
+    _: true 
+  }
diff --git a/book/U60.fib.kind2 b/book/U60/fib.kind2
similarity index 100%
rename from book/U60.fib.kind2
rename to book/U60/fib.kind2
diff --git a/book/U60/from_nat.kind2 b/book/U60/from_nat.kind2
new file mode 100644
index 000000000..d27ae0377
--- /dev/null
+++ b/book/U60/from_nat.kind2
@@ -0,0 +1,7 @@
+use Nat/{succ,zero}
+
+from_nat (n: Nat) : U60 =
+  match n {
+    succ: (+ 1 (from_nat n.pred))
+    zero: 0
+  }
diff --git a/book/U60/if.kind2 b/book/U60/if.kind2
new file mode 100644
index 000000000..8c8719906
--- /dev/null
+++ b/book/U60/if.kind2
@@ -0,0 +1,5 @@
+if <P> (x: U60) (t: P) (f: P) : P =
+  switch x {
+    0: t
+    _: f
+  }
diff --git a/book/U60/match.kind2 b/book/U60/match.kind2
new file mode 100644
index 000000000..47a2697e2
--- /dev/null
+++ b/book/U60/match.kind2
@@ -0,0 +1,5 @@
+U60.match (x: U60) (P: U60 -> *) (s: U60 -> (P (+ 1 x))) (z: (P 0)) : (P x) =
+  switch x {
+    0: z
+    _: (s x-1)
+  }: (P x)
diff --git a/book/U60/max.kind2 b/book/U60/max.kind2
new file mode 100644
index 000000000..a59f1dc8c
--- /dev/null
+++ b/book/U60/max.kind2
@@ -0,0 +1,5 @@
+max (a: U60) (b: U60) : U60 =
+  switch x = (< a b) {
+    0: a
+    _: b
+  }
diff --git a/book/U60/min.kind2 b/book/U60/min.kind2
new file mode 100644
index 000000000..ece5af6ad
--- /dev/null
+++ b/book/U60/min.kind2
@@ -0,0 +1,5 @@
+min (a: U60) (b: U60) : U60 =
+  switch x = (< a b) {
+    0: b
+    _: a
+  }
diff --git a/book/U60/name.kind2 b/book/U60/name.kind2
new file mode 100644
index 000000000..fb081d251
--- /dev/null
+++ b/book/U60/name.kind2
@@ -0,0 +1,2 @@
+U60.name (n: U60) : String =
+  (String/Chunk/build (U60/name/go (+ n 1)))
diff --git a/book/U60.name.go.kind2 b/book/U60/name/go.kind2
similarity index 71%
rename from book/U60.name.go.kind2
rename to book/U60/name/go.kind2
index c356d0724..cd051c25b 100644
--- a/book/U60.name.go.kind2
+++ b/book/U60/name/go.kind2
@@ -1,5 +1,5 @@
 U60.name.go
-: ∀(n: U60) String.Concatenator
+: ∀(n: U60) String.Chunk
 = λn
   switch n = n {
     0: λnil nil
@@ -8,4 +8,4 @@ U60.name.go
       (+ 97 (% n-1 26))
       (U60.name.go (/ n-1 26) nil)
     ) 
-  }: String.Concatenator
\ No newline at end of file
+  }: String.Chunk
\ No newline at end of file
diff --git a/book/U60.parser.decimal.kind2 b/book/U60/parser/decimal.kind2
similarity index 100%
rename from book/U60.parser.decimal.kind2
rename to book/U60/parser/decimal.kind2
diff --git a/book/U60/show.kind2 b/book/U60/show.kind2
new file mode 100644
index 000000000..e4af9f758
--- /dev/null
+++ b/book/U60/show.kind2
@@ -0,0 +1,2 @@
+U60.show (n: U60) : String =
+  (String/Chunk/build (U60/show/go n))
diff --git a/book/U60/show/go.kind2 b/book/U60/show/go.kind2
new file mode 100644
index 000000000..22e6d5313
--- /dev/null
+++ b/book/U60/show/go.kind2
@@ -0,0 +1,5 @@
+go (n: U60) : String/Chunk =
+  switch x = (< n 10) {
+    0: λnil (go (/ n 10) (String/cons (+ 48 (% n 10)) nil))
+    _: λnil (String/cons (+ 48 n) nil) 
+  }
diff --git a/book/U60.sum.kind2 b/book/U60/sum.kind2
similarity index 100%
rename from book/U60.sum.kind2
rename to book/U60/sum.kind2
diff --git a/book/U60/to_bool.kind2 b/book/U60/to_bool.kind2
new file mode 100644
index 000000000..dfb086101
--- /dev/null
+++ b/book/U60/to_bool.kind2
@@ -0,0 +1,7 @@
+use Bool/{true,false}
+
+to_bool (x: U60) : Bool =
+  switch x {
+    0: false
+    _: true
+  }: Bool
diff --git a/book/Unit.kind2 b/book/Unit.kind2
index 462aea14c..de2be9eed 100644
--- a/book/Unit.kind2
+++ b/book/Unit.kind2
@@ -1,4 +1,2 @@
-Unit
-: *
-= $(self: Unit)
-  ∀(P: ∀(x: Unit) *) ∀(one: (P Unit.one)) (P self)
\ No newline at end of file
+data Unit
+| new
diff --git a/book/Unit.match.kind2 b/book/Unit.match.kind2
deleted file mode 100644
index fb3d69d06..000000000
--- a/book/Unit.match.kind2
+++ /dev/null
@@ -1,4 +0,0 @@
-Unit.switch
-: ∀(x: Unit) ∀(P: ∀(x: Unit) *) ∀(o: (P Unit.one))
-  (P x)
-= λx λP λo (~x P o)
\ No newline at end of file
diff --git a/book/Unit.one.kind2 b/book/Unit.one.kind2
deleted file mode 100644
index 240f1179c..000000000
--- a/book/Unit.one.kind2
+++ /dev/null
@@ -1,3 +0,0 @@
-Unit.one
-: Unit
-= ~λP λone one
\ No newline at end of file
diff --git a/book/Unit/match.kind2 b/book/Unit/match.kind2
new file mode 100644
index 000000000..35df99623
--- /dev/null
+++ b/book/Unit/match.kind2
@@ -0,0 +1,4 @@
+Unit.match
+  (x: Unit) (P: Unit -> *) (new: (P Unit.new))
+: (P x)
+= (~x P new)
diff --git a/book/Unit/new.kind2 b/book/Unit/new.kind2
new file mode 100644
index 000000000..88709608f
--- /dev/null
+++ b/book/Unit/new.kind2
@@ -0,0 +1,2 @@
+Unit.new : Unit =
+  ~λP λone one
diff --git a/book/Vector.cons.kind2 b/book/Vector.cons.kind2
deleted file mode 100644
index cae946397..000000000
--- a/book/Vector.cons.kind2
+++ /dev/null
@@ -1,3 +0,0 @@
-Vector.cons
-: ∀(T: *) ∀(len: Nat) ∀(head: T) ∀(tail: (Vector T len)) (Vector T (Nat.succ len))
-= λT λlen λhead λtail ~λP λcons λnil (cons len head tail)
diff --git a/book/Vector.kind2 b/book/Vector.kind2
index eef518aad..11351373c 100644
--- a/book/Vector.kind2
+++ b/book/Vector.kind2
@@ -1,3 +1,3 @@
 data Vector T (len: Nat)
-| cons (len: Nat) (head: T) (tail: (Vector T len)) : (Vector T (Nat.succ len))
-| nil : (Vector T Nat.zero)
+| cons (len: Nat) (head: T) (tail: (Vector T len)) : (Vector T (Nat/succ len))
+| nil : (Vector T Nat/zero)
diff --git a/book/Vector.nil.kind2 b/book/Vector.nil.kind2
deleted file mode 100644
index 5eeabecf8..000000000
--- a/book/Vector.nil.kind2
+++ /dev/null
@@ -1,3 +0,0 @@
-Vector.nil
-: ∀(T: *) (Vector T Nat.zero)
-= λT ~λP λcons λnil nil
diff --git a/book/Vector.concat.kind2 b/book/Vector/concat.kind2
similarity index 70%
rename from book/Vector.concat.kind2
rename to book/Vector/concat.kind2
index 9b541d524..08a34a528 100644
--- a/book/Vector.concat.kind2
+++ b/book/Vector/concat.kind2
@@ -1,13 +1,13 @@
-use Vector.{cons,nil}
-use Nat.{succ,zero,add}
+use Vector/{cons,nil}
+use Nat/{succ,zero,add}
 
-concat T (xs_len: Nat) (ys_len: Nat)
+concat <T> (xs_len: Nat) (ys_len: Nat)
   (xs: (Vector T xs_len))
   (ys: (Vector T ys_len))
 : (Vector T (add xs_len ys_len))
 = match xs {
-    cons : (cons T (add xs.len ys_len) xs.head (concat T xs.len ys_len xs.tail ys))
-    nil  : ys
+    cons: (cons (add xs.len ys_len) xs.head (concat xs.len ys_len xs.tail ys))
+    nil: ys
   }
 
 //concat
diff --git a/book/Vector/cons.kind2 b/book/Vector/cons.kind2
new file mode 100644
index 000000000..a94312600
--- /dev/null
+++ b/book/Vector/cons.kind2
@@ -0,0 +1,2 @@
+cons <T> (len: Nat) (head: T) (tail: (Vector T len)) : (Vector T (Nat/succ len)) =
+  ~ λP λcons λnil (cons len head tail)
diff --git a/book/Vector/nil.kind2 b/book/Vector/nil.kind2
new file mode 100644
index 000000000..a01c6134d
--- /dev/null
+++ b/book/Vector/nil.kind2
@@ -0,0 +1,2 @@
+nil <T> : (Vector T Nat/zero) =
+  ~λP λcons λnil nil
diff --git a/book/script.js b/book/script.js
new file mode 100644
index 000000000..f94065a32
--- /dev/null
+++ b/book/script.js
@@ -0,0 +1,32 @@
+const fs = require('fs');
+const path = require('path');
+
+// Read all .kind2 files in the current directory
+fs.readdir('.', (err, files) => {
+  if (err) {
+    console.error('Error reading directory:', err);
+    return;
+  }
+
+  files.filter(file => file.endsWith('.kind2')).forEach(file => {
+    // Construct new path by replacing dots with slashes, except for the extension
+    const newName = file.slice(0, -6).replace(/\./g, '/') + file.slice(-6);
+    const newPath = path.join('.', newName);
+    const newDir = path.dirname(newPath);
+
+    // Create the directory structure if it doesn't exist
+    fs.mkdir(newDir, { recursive: true }, (err) => {
+      if (err) {
+        console.error('Error creating directories:', err);
+        return;
+      }
+
+      // Move the file to the new location
+      fs.rename(file, newPath, (err) => {
+        if (err) {
+          console.error('Error moving file:', err);
+        }
+      });
+    });
+  });
+});
diff --git a/src/book/mod.rs b/src/book/mod.rs
index 7cc948ff5..334ead787 100644
--- a/src/book/mod.rs
+++ b/src/book/mod.rs
@@ -26,7 +26,7 @@ pub fn shadow(key: &str, uses: &Uses) -> Uses {
   return uses;
 }
 
-// Maps short names ("cons") to full names ("Data.List.cons")
+// Maps short names ("cons") to full names ("List/cons")
 pub type Uses = im::HashMap<String, String>;
 
 impl Book {
@@ -44,11 +44,11 @@ impl Book {
     let mut book = Book::new();
     book.load(base, name)?;
     book.load(base, "String")?;
-    book.load(base, "String.cons")?;
-    book.load(base, "String.nil")?;
+    book.load(base, "String/cons")?;
+    book.load(base, "String/nil")?;
     book.load(base, "Nat")?;
-    book.load(base, "Nat.succ")?;
-    book.load(base, "Nat.zero")?;
+    book.load(base, "Nat/succ")?;
+    book.load(base, "Nat/zero")?;
     book.expand_implicits();
     return Ok(book);
   }
@@ -60,6 +60,7 @@ impl Book {
 
   // Same as load, mutably adding to a 'book'
   pub fn load(&mut self, base: &str, name: &str) -> Result<(), String> {
+    let name = name.trim_end_matches('/'); // last "/" is not part of name
     if !self.defs.contains_key(name) {
       // Parses a file into a new book
       let file = format!("{}/{}.kind2", base, name);
diff --git a/src/book/parse.rs b/src/book/parse.rs
index cc279ae3a..8a393a9e0 100644
--- a/src/book/parse.rs
+++ b/src/book/parse.rs
@@ -21,7 +21,7 @@ impl<'i> KindParser<'i> {
         }
       }
     } else {
-      let pts = nam.split('.').collect::<Vec<&str>>();
+      let pts = nam.split('/').collect::<Vec<&str>>();
       let key = pts.last().unwrap().to_string();
       //println!("use {} ~> {}", key, nam);
       uses.insert(key, nam);
@@ -128,7 +128,7 @@ impl<'i> KindParser<'i> {
     // Parses all top-level 'use' declarations.
     let mut uses = self.parse_uses(fid)?;
     // Each file has an implicit 'use Path.to.file'. We add it here:
-    uses.insert(name.split('.').last().unwrap().to_string(), name.to_string());
+    uses.insert(name.split('/').last().unwrap().to_string(), name.to_string());
     // Parses all definitions.
     while *self.index() < self.input().len() {
       let (name, term) = self.parse_def(fid, &mut uses)?;
@@ -153,50 +153,62 @@ impl Term {
 
   // Wraps many lams around this term. Linearizes when possible.
   fn add_lams(&mut self, args: im::Vector<(bool,String,Term)>) {
-    // Passes through Src
-    if let Term::Src { val, .. } = self {
-      val.add_lams(args);
-      return;
-    }
-    // Passes through Ann
-    if let Term::Ann { val, .. } = self {
-      val.add_lams(args);
-      return;
-    }
-    // Linearizes a numeric pattern match
-    if let Term::Swi { nam, z, s, .. } = self {
-      if args.len() >= 1 && args[0].1 == *nam {
-        let (head, tail) = args.split_at(1);
-        z.add_lams(tail.clone());
-        s.add_lams(tail.clone());
-        self.add_lam(head[0].0, &head[0].1);
-        return;
-      }
-    }
-    // Linearizes a user-defined ADT match
-    if let Term::Mch { mch } = self {
-      if !mch.fold {
-        let Match { name, cses, .. } = &mut **mch;
-        if args.len() >= 1 && args[0].1 == *name {
-          let (head, tail) = args.split_at(1);
-          for (_, cse) in cses {
-            cse.add_lams(tail.clone());
-          }
-          self.add_lam(head[0].0, &head[0].1);
-          return;
-        }
-      }
-    }
-    // Prepend remaining lambdas
-    if args.len() > 0 {
-      let (head, tail) = args.split_at(1);
-      self.add_lam(head[0].0, &head[0].1);
-      if let Term::Lam { era: _, nam: _, bod } = self {
-        bod.add_lams(tail.clone());
-      } else {
-        unreachable!();
-      }
+    for (era, nam, _) in args.iter().rev() {
+      self.add_lam(*era, &nam);
     }
+
+    // NOTE: match-passthrough removed due to problems. For example:
+    // U60.if (x: U60) (P: *) (t: P) (f: P) : P = switch x { 0: t _: f }
+    // This wouldn't check, because 'P' is moved inside, becoming a different 'P'.
+    // I think automatic behaviors like this are dangerous and should be avoided.
+
+    //// Passes through Src
+    //if let Term::Src { val, .. } = self {
+      //val.add_lams(args);
+      //return;
+    //}
+    //// Passes through Ann
+    //if let Term::Ann { val, .. } = self {
+      //val.add_lams(args);
+      //return;
+    //}
+    //// Linearizes a numeric pattern match
+    //if let Term::Swi { nam, z, s, p, .. } = self {
+      //if args.len() >= 1 && args[0].1 == *nam {
+        //let (head, tail) = args.split_at(1);
+        //z.add_lams(tail.clone());
+        //s.add_lams(tail.clone());
+        //p.add_alls(tail.clone());
+        //self.add_lam(head[0].0, &head[0].1);
+        //return;
+      //}
+    //}
+    //// Linearizes a user-defined ADT match
+    //if let Term::Mch { mch } = self {
+      //if !mch.fold {
+        //let Match { name, cses, moti, .. } = &mut **mch;
+        //if args.len() >= 1 && args[0].1 == *name {
+          //let (head, tail) = args.split_at(1);
+          //for (_, cse) in cses {
+            //cse.add_lams(tail.clone());
+          //}
+          //moti.as_mut().map(|x| x.add_alls(tail.clone()));
+          //self.add_lam(head[0].0, &head[0].1);
+          //return;
+        //}
+      //}
+    //}
+    //// Prepend remaining lambdas
+    //if args.len() > 0 {
+      //let (head, tail) = args.split_at(1);
+      //self.add_lam(head[0].0, &head[0].1);
+      //if let Term::Lam { era: _, nam: _, bod } = self {
+        //bod.add_lams(tail.clone());
+      //} else {
+        //unreachable!();
+      //}
+    //}
+  
   }
 
   // Wraps an All around this term.
diff --git a/src/sugar/mod.rs b/src/sugar/mod.rs
index 8a1a48820..a29ef9173 100644
--- a/src/sugar/mod.rs
+++ b/src/sugar/mod.rs
@@ -54,7 +54,7 @@ pub struct Match {
 //
 // The List sugar is merely a shortcut. For example:
 //
-//   (List.cons _ a (List.cons _ b (List.cons _ c (List.nil _))))
+//   (List/cons _ a (List/cons _ b (List/cons _ c (List/nil _))))
 //
 // Is converted to and from:
 //    
@@ -233,10 +233,10 @@ impl Term {
 impl Term {
 
   // Interprets as a list:
-  // - (((List.cons _) x) (((List.cons _) y) ... (List.nil _)))
+  // - (((List/cons _) x) (((List/cons _) y) ... (List/nil _)))
   // Patterns:
-  // - (CONS head tail) ::= (App (App (App (Var "List.cons") Met) head) tail)
-  // - NIL              ::= (App (Var "List.nil") Met)
+  // - (CONS head tail) ::= (App (App (App (Var "List/cons") Met) head) tail)
+  // - NIL              ::= (App (Var "List/nil") Met)
   pub fn as_list(&self) -> Option<List> {
     let mut vals = Vec::new();
     let mut term = self;
@@ -246,7 +246,7 @@ impl Term {
           if let Term::App { era: _, fun: cons, arg: head } = &**fun {
             if let Term::App { era: _, fun: cons_fun, arg: _ } = &**cons {
               if let Term::Var { nam } = &**cons_fun {
-                if nam == "List.cons" {
+                if nam == "List/cons" {
                   vals.push(head.clone());
                   term = arg;
                   continue;
@@ -255,7 +255,7 @@ impl Term {
             }
           }
           if let Term::Var { nam } = &**fun {
-            if nam == "List.nil" {
+            if nam == "List/nil" {
               return Some(List { vals });
             }
           }
@@ -266,23 +266,15 @@ impl Term {
     }
   }
 
-  // Builds a chain of applications of List.cons and List.nil from a Vec<Box<Term>>
+  // Builds a chain of applications of List/cons and List/nil from a Vec<Box<Term>>
   pub fn new_list(list: &List) -> Term {
-    let mut term = Term::App {
-      era: true,
-      fun: Box::new(Term::Var { nam: "List.nil".to_string() }),
-      arg: Box::new(Term::Met {}),
-    };
+    let mut term = Term::Var { nam: "List/nil".to_string() };
     for item in (&list.vals).into_iter().rev() {
       term = Term::App {
         era: false,
         fun: Box::new(Term::App {
           era: false,
-          fun: Box::new(Term::App {
-            era: true,
-            fun: Box::new(Term::Var { nam: "List.cons".to_string() }),
-            arg: Box::new(Term::Met {}),
-          }),
+          fun: Box::new(Term::Var { nam: "List/cons".to_string() }),
           arg: item.clone(),
         }),
         arg: Box::new(term),
@@ -377,15 +369,9 @@ impl Equal {
   
   pub fn format(&self) -> Box<Show> {
     Show::glue(" ", vec![
-      Show::glue("", vec![
-        Show::text("{"),
-        self.a.format_go(),
-      ]),
-      Show::text("="),
-      Show::glue("", vec![
-        self.b.format_go(),
-        Show::text("}"),
-      ]),
+      self.a.format_go(),
+      Show::text("=="),
+      self.b.format_go(),
     ])
   }
 
@@ -608,17 +594,17 @@ impl Term {
       }
 
       // Builds the constructor type: (Type.C0 P0 P1 ... C0_F0 C0_F1 ...)
-      let mut ctr_type = Term::Var { nam: format!("{}.{}", adt.name, ctr.name) };
+      let mut ctr_type = Term::Var { nam: format!("{}/{}/", adt.name, ctr.name) };
 
       // For each type parameter
       // NOTE: Not necessary anymore due to auto implicit arguments
-      //for par in adt.pars.iter() {
-        //ctr_type = Term::App {
-          //era: true,
-          //fun: Box::new(ctr_type),
-          //arg: Box::new(Term::Var { nam: par.clone() }),
-        //};
-      //}
+      for par in adt.pars.iter() {
+        ctr_type = Term::App {
+          era: true,
+          fun: Box::new(ctr_type),
+          arg: Box::new(Term::Var { nam: par.clone() }),
+        };
+      }
 
       // And for each field
       for (fld_name, _fld_type) in ctr.flds.iter() {
@@ -904,7 +890,7 @@ impl Term {
     for ctr in &adt.ctrs {
       // Find this constructor's case
       let found = mat.cses.iter().find(|(case_name, _)| {
-        return case_name == &format!("{}.{}", adt.name, ctr.name);
+        return case_name == &format!("{}/{}", adt.name, ctr.name);
       });
       if let Some((_, case_term)) = found {
         // If it is present...
@@ -933,31 +919,32 @@ impl Term {
       }
     }
 
-    // 3. Wrap Ins or Type.fold around term
+    // 3. Make `(~x <motive>)` or `(Type/fold/ _ <motive> x)`
     if mat.fold {
       term = Term::App {
-        era: false,
+        era: true,
         fun: Box::new(Term::App {
-          era: true,
-          fun: Box::new(Term::Var { nam: format!("{}.fold", adt.name) }),
-          arg: Box::new(Term::Met {}),
+          era: false,
+          fun: Box::new(Term::App {
+            era: true,
+            fun: Box::new(Term::Var { nam: format!("{}/fold/", adt.name) }),
+            arg: Box::new(Term::Met {}),
+          }),
+          arg: Box::new(Term::Var { nam: format!("{}.P", mat.name) }),
         }),
-        arg: Box::new(mat.expr.clone()),
+        arg: Box::new(mat.expr.clone())
       };
     } else {
-      term = Term::Ins {
-        val: Box::new(mat.expr.clone())
+      term = Term::App {
+        era: true,
+        fun: Box::new(Term::Ins {
+          val: Box::new(mat.expr.clone())
+        }),
+        arg: Box::new(Term::Var { nam: format!("{}.P", mat.name) }),
       };
     }
 
-    // 4. Apply the motive, making a Var for it
-    term = Term::App {
-      era: true,
-      fun: Box::new(term),
-      arg: Box::new(Term::Var { nam: format!("{}.P", mat.name) }),
-    };
-
-    // 5. Apply each constructor (by name)
+    // 4. Apply each constructor (by name)
     for ctr in &adt.ctrs {
       term = Term::App {
         era: false,
@@ -966,7 +953,7 @@ impl Term {
       };
     }
 
-    // 6. Annotates with the moved var foralls
+    // 5. Annotates with the moved var foralls
     if mat.with.len() > 0 {
       let mut ann_type = Term::Met {};
       for (nam, typ) in mat.with.iter().rev() {
@@ -984,7 +971,7 @@ impl Term {
       };
     }
 
-    // 7. Applies each moved var
+    // 6. Applies each moved var
     for (nam, _) in mat.with.iter() {
       term = Term::App {
         era: false,
@@ -993,7 +980,7 @@ impl Term {
       };  
     }
 
-    // 8. Create the local 'use' definition for each term
+    // 7. Create the local 'use' definition for each term
     for (i,ctr) in adt.ctrs.iter().enumerate().rev() {
       term = Term::Use {
         nam: format!("{}.{}", mat.name, ctr.name),
@@ -1002,14 +989,14 @@ impl Term {
       };
     }
 
-    // 9. Create the local 'use' definition for the motive
+    // 8. Create the local 'use' definition for the motive
     term = Term::Use {
       nam: format!("{}.P", mat.name),
       val: Box::new(motive),
       bod: Box::new(term)
     };
 
-    // 10. Return 'term'
+    // 9. Return 'term'
     return term;
   }
 
@@ -1084,28 +1071,37 @@ impl<'i> KindParser<'i> {
     let mut adt = "Empty".to_string();
     let mut cses = Vec::new();
     while self.peek_one() != Some('}') {
-      let cse_name = self.parse_name()?;
+      self.skip_trivia();
+      let cse_name = if self.peek_many(2) == Some("++") {
+        self.consume("++")?;
+        "List/cons".to_string()
+      } else if self.peek_many(2) == Some("[]") {
+        self.consume("[]")?;
+        "List/nil".to_string()
+      } else {
+        self.parse_name()?
+      };
       let cse_name = uses.get(&cse_name).unwrap_or(&cse_name).to_string();
       // Infers the local ADT name
       let adt_name = {
-        let pts = cse_name.split('.').collect::<Vec<&str>>();
+        let pts = cse_name.split('/').collect::<Vec<&str>>();
         if pts.len() < 2 {
-          return self.expected(&format!("valid constructor (did you forget 'TypeName.' before '{}'?)", cse_name));
+          return self.expected(&format!("valid constructor (did you forget 'TypeName/' before '{}'?)", cse_name));
         } else {
-          pts[..pts.len() - 1].join(".")
+          pts[..pts.len() - 1].join("/")
         }
       };
       // Sets the global ADT name
       if adt == "Empty" {
         adt = adt_name.clone();
       } else if adt != adt_name {
-        return self.expected(&format!("{}.constructor", adt));
+        return self.expected(&format!("{}/constructor", adt));
       }
       // Finds this case's constructor
-      let cnm = cse_name.split('.').last().unwrap().to_string();
+      let cnm = cse_name.split('/').last().unwrap().to_string();
       let ctr = ADT::load(&adt).ok().and_then(|adt| adt.ctrs.iter().find(|ctr| ctr.name == cnm).cloned());
       if ctr.is_none() {
-        return self.expected(&format!("a valid constructor ({}.{} doesn't exit)", adt_name, cnm));
+        return self.expected(&format!("a valid constructor ({}/{} doesn't exit)", adt_name, cnm));
       }
       // Shadows this constructor's field variables
       let mut uses = uses.clone();
diff --git a/src/term/compile.rs b/src/term/compile.rs
index a2ce4d820..d0457f9f9 100644
--- a/src/term/compile.rs
+++ b/src/term/compile.rs
@@ -157,7 +157,7 @@ impl Term {
   }
 
   pub fn to_hs_name(name: &str) -> String {
-    format!("x{}", name.replace("-", "_").replace(".","_"))
+    format!("x{}", name.replace("-", "_").replace(".","_").replace("/","_"))
   }
 
   pub fn to_hs_checker(&self, env: im::Vector<String>, met: &mut usize) -> String {
diff --git a/src/term/mod.rs b/src/term/mod.rs
index 2bd3784b9..e3e6d13c6 100644
--- a/src/term/mod.rs
+++ b/src/term/mod.rs
@@ -392,7 +392,11 @@ impl Term {
         val.expand_implicits(env, implicit_count);
       },
       Term::Var { nam } => {
-        if !env.contains(nam) {
+        // When a name ends with "/", it must apply its implicits manually
+        if nam.ends_with("/") {
+          *self = Term::Var { nam: nam.trim_end_matches('/').to_string() };
+        // Otherwise, we apply its implicits, turning 'F' into '(F _ _ ...)'
+        } else if !env.contains(nam) {
           if let Some(implicits) = implicit_count.get(nam) {
             for _ in 0..*implicits {
               *self = Term::App {
diff --git a/src/term/parse.rs b/src/term/parse.rs
index 6e908636a..5563e639d 100644
--- a/src/term/parse.rs
+++ b/src/term/parse.rs
@@ -124,7 +124,7 @@ impl<'i> KindParser<'i> {
       return Ok(Term::Src { src, val: Box::new(Term::Lam { era, nam, bod }) });
     }
 
-    // RFL ::= (=)
+    // RFL ::= {=}
     if self.starts_with("{=}") {
       let ini = *self.index() as u64;
       self.consume("{=}")?;
@@ -134,11 +134,7 @@ impl<'i> KindParser<'i> {
         src,
         val: Box::new(Term::App {
           era: false,
-          fun: Box::new(Term::App {
-            era: false,
-            fun: Box::new(Term::Var { nam: "Equal.refl".to_string() }),
-            arg: Box::new(Term::Met {}),
-          }),
+          fun: Box::new(Term::Var { nam: "Equal/refl".to_string() }),
           arg: Box::new(Term::Met {}),
         })
       });
@@ -492,8 +488,8 @@ impl<'i> KindParser<'i> {
     }
 
     // List.cons
-    if self.starts_with(",") {
-      self.consume(",")?;
+    if self.starts_with("++") {
+      self.consume("++")?;
       let ini = *self.index() as u64;
       let hd  = Box::new(term);
       let tl  = Box::new(self.parse_term(fid, uses)?);
@@ -505,11 +501,7 @@ impl<'i> KindParser<'i> {
           era: false,
           fun: Box::new(Term::App {
             era: false,
-            fun: Box::new(Term::App {
-              era: true,
-              fun: Box::new(Term::Var { nam: "cons".to_string() }),
-              arg: Box::new(Term::Met {}),
-            }),
+            fun: Box::new(Term::Var { nam: "List/cons".to_string() }),
             arg: hd,
           }),
           arg: tl,
diff --git a/src/term/show.rs b/src/term/show.rs
index 23b669e9e..611a24fdf 100644
--- a/src/term/show.rs
+++ b/src/term/show.rs
@@ -115,16 +115,10 @@ impl Term {
       }
       Term::Ann { chk: _, val, typ: _ } => {
         val.format_go()
-        //Show::call("", vec![
-          //Show::glue("", vec![
-            //Show::text("{"),
-            //val.format_go(),
-          //]),
-          //Show::glue("", vec![
-            //Show::text(":"),
-            //typ.format_go(),
-            //Show::text("}"),
-          //])
+        //Show::call(" ", vec![
+          //val.format_go(),
+          //Show::text("::"),
+          //typ.format_go(),
         //])
       },
       Term::Slf { nam, typ, bod } => {