Merge branch 'master' of https://github.com/Derenash/kind2.0

2024-10-03 18:27:13 +03:00 · 2024-03-14 16:31:59 -03:00 · 2024-03-14 16:31:59 -03:00 · f4be6b5e45
commit f4be6b5e45
parent 357cc111a6 2666e5de0e
100 changed files with 434 additions and 559 deletions
--- a/book/A.kind2
+++ b/book/A.kind2
@ -1,13 +0,0 @@
-A : * =
-  $(self: A)
-  ∀(P: ∀(x: A) *)
-  ∀(s: ∀(t: ∀(T: *) ∀(k: ∀(pred: A) T) T) (P (t A A.succ)))
-  ∀(z: ∀(t: ∀(T: *) ∀(k: T) T) (P (t A A.zero)))
-  (P self)
-
-  //∀(k: ∀(x: X) ∀(y: Y) (P (K x y)))
-  //-------------------------------------
-  //∀(k: ∀(p: (X,Y)) (P (p λxλy(K x y))))
-  //-------------------------------------
-  //∀(k: ∀(p: Σ(x:X) Σ(y:Y) ()) (P (p λxλy(K x y))))
-
--- a/book/A.succ.kind2
+++ b/book/A.succ.kind2
@ -1,3 +0,0 @@
-A.succ : ∀(p: A) A =
-  λp
-  ~λP λs λz (s λTλt(t p))
--- a/book/A.zero.kind2
+++ b/book/A.zero.kind2
@ -1,2 +0,0 @@
-A.zero : A =
-  ~λP λs λz (z λTλt(t))
--- a/book/BBT.balance.kind2
+++ b/book/BBT.balance.kind2
@ -13,10 +13,10 @@ BBT.balance
  use new = λlft.size λlft
    use P = λx (BBT K V)
    use new = λrgt.size λrgt
-      use new_size = #(+ #1 (U60.max lft.size rgt.size))
+      use new_size = (+ 1 (U60.max lft.size rgt.size))
      use balance = (U60.abs_diff lft.size rgt.size)
      use P = λx
-        ∀(new_size: #U60)
+        ∀(new_size: U60)
        ∀(node_key: K)
        ∀(val: V)
        ∀(lft: (BBT K V))
@ -27,7 +27,7 @@ BBT.balance
          ∀(K: *)
          ∀(V: *)
          ∀(cmp: ∀(a: K) ∀(b: K) Cmp)
-          ∀(new_size: #U60)
+          ∀(new_size: U60)
          ∀(node_key: K)
          ∀(set_key: K)
          ∀(val: V)
@ -36,7 +36,7 @@ BBT.balance
          (BBT K V)
        use true = BBT.balance.lft_heavier
        use false = BBT.balance.rgt_heavier
-        (~(U60.to_bool #(< rgt.size lft.size))
+        (~(U60.to_bool (< rgt.size lft.size))
          P
          true
          false
@ -52,7 +52,7 @@ BBT.balance
        )
      use false = λnew_size λnode_key λval λlft λrgt
        (BBT.bin K V new_size node_key val lft rgt)
-      (~(U60.to_bool #(> balance #1))
+      (~(U60.to_bool (> balance 1))
        P
        true
        false
--- a/book/BBT.balance.lft_heavier.kind2
+++ b/book/BBT.balance.lft_heavier.kind2
@ -2,7 +2,7 @@ BBT.balance.lft_heavier
 : ∀(K: *)
  ∀(V: *)
  ∀(cmp: ∀(a: K) ∀(b: K) Cmp)
-  ∀(new_size: #U60)
+  ∀(new_size: U60)
  ∀(node_key: K)
  ∀(set_key: K)
  ∀(val: V)
@ -13,7 +13,7 @@ BBT.balance.lft_heavier
  use P = λx (BBT K V)
  use bin = λlft.size λlft.key λlft.val λlft.lft λlft.rgt
    use P = λx
-      ∀(new_size: #U60)
+      ∀(new_size: U60)
      ∀(key: K)
      ∀(val: V)
      ∀(lft.key: K)
--- a/book/BBT.balance.rgt_heavier.kind2
+++ b/book/BBT.balance.rgt_heavier.kind2
@ -2,7 +2,7 @@ BBT.balance.rgt_heavier
 : ∀(K: *)
  ∀(V: *)
  ∀(cmp: ∀(a: K) ∀(b: K) Cmp)
-  ∀(new_size: #U60)
+  ∀(new_size: U60)
  ∀(node_key: K)
  ∀(set_key: K)
  ∀(val: V)
@ -13,7 +13,7 @@ BBT.balance.rgt_heavier
  use P = λx (BBT K V)
  use bin = λrgt.size λrgt.key λrgt.val λrgt.lft λrgt.rgt
    use P = λx
-      ∀(new_size: #U60)
+      ∀(new_size: U60)
      ∀(key: K)
      ∀(val: V)
      ∀(lft: (BBT K V))
--- a/book/BBT.bin.kind2
+++ b/book/BBT.bin.kind2
@ -1,7 +1,7 @@
 BBT.bin
 : ∀(K: *)
  ∀(V: *)
-  ∀(size: #U60)
+  ∀(size: U60)
  ∀(key: K)
  ∀(val: V)
  ∀(lft: (BBT K V))
--- a/book/BBT.got_size.kind2
+++ b/book/BBT.got_size.kind2
@ -1,10 +1,10 @@
 BBT.got_size
 : ∀(K: *) ∀(V: *) ∀(map: (BBT K V))
-  (Pair #U60 (BBT K V))
+  (Pair U60 (BBT K V))
 = λK λV λmap
-  use P = λx (Pair #U60 (BBT K V))
+  use P = λx (Pair U60 (BBT K V))
  use bin = λsize λnext.key λnext.val λnext.lft λnext.rgt
    use map = (BBT.bin K V size next.key next.val next.lft next.rgt)
-    (Pair.new #U60 (BBT K V) size map)
-  use tip = (Pair.new #U60 (BBT K V) #0 (BBT.tip K V))
+    (Pair.new U60 (BBT K V) size map)
+  use tip = (Pair.new U60 (BBT K V) 0 (BBT.tip K V))
  (~map P bin tip)
--- a/book/BBT.kind2
+++ b/book/BBT.kind2
@ -4,7 +4,7 @@ BBT
  $(self: (BBT K V))
  ∀(P: ∀(bbt: (BBT K V)) *)
  ∀(bin: 
-    ∀(size: #U60)
+    ∀(size: U60)
    ∀(key: K)
    ∀(val: V)
    ∀(lft: (BBT K V))
--- a/book/BBT.lft_rotate.kind2
+++ b/book/BBT.lft_rotate.kind2
@ -1,7 +1,7 @@
 BBT.lft_rotate
 : ∀(K: *)
  ∀(V: *)
-  ∀(size: #U60)
+  ∀(size: U60)
  ∀(key: K)
  ∀(val: V)
  ∀(lft: (BBT K V))
@ -15,4 +15,4 @@ BBT.lft_rotate
    a
  use tip = λkey λval λlft
    (BBT.bin K V size key val lft (BBT.tip K V))
-  (~rgt P bin tip key val lft)
+  (~rgt P bin tip key val lft)
--- a/book/BBT.new_node.kind2
+++ b/book/BBT.new_node.kind2
@ -11,7 +11,7 @@ BBT.new_node
  use new = λlft.size λlft
    use P = λx (BBT K V)
    use new = λrgt.size λrgt
-      use new_size = #(+ #1 (U60.max rgt.size lft.size))
+      use new_size = (+ 1 (U60.max rgt.size lft.size))
      (BBT.bin K V new_size key val lft rgt)
    (~(BBT.got_size K V rgt) P new)
-  (~(BBT.got_size K V lft) P new)
+  (~(BBT.got_size K V lft) P new)
--- a/book/BBT.rgt_rotate.kind2
+++ b/book/BBT.rgt_rotate.kind2
@ -1,7 +1,7 @@
 BBT.rgt_rotate
 : ∀(K: *)
  ∀(V: *)
-  ∀(size: #U60)
+  ∀(size: U60)
  ∀(key: K)
  ∀(val: V)
  ∀(lft: (BBT K V))
--- a/book/BBT.singleton.kind2
+++ b/book/BBT.singleton.kind2
@ -1,4 +1,4 @@
 BBT.singleton
 : ∀(K: *) ∀(V: *) ∀(key: K) ∀(val: V) (BBT K V)
 = λK λV λkey λval
-  (BBT.bin K V #1 key val (BBT.tip K V) (BBT.tip K V))
+  (BBT.bin K V 1 key val (BBT.tip K V) (BBT.tip K V))
--- a/book/Bool.lemma.notnot.kind2
+++ b/book/Bool.lemma.notnot.kind2
@ -2,6 +2,6 @@ use Bool.{true,false,not}

 notnot (x: Bool) : {(not (not x)) = x} =
  match x {
-    true  : {=}
-    false : {=}
+    true: {=}
+    false: {=}
  }
--- a/book/Char.escapes.kind2
+++ b/book/Char.escapes.kind2
@ -1,14 +1,14 @@
 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)
+  (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)
 ]
--- a/book/Char.is_between.kind2
+++ b/book/Char.is_between.kind2
@ -1,5 +1,5 @@
 Char.is_between (min: Char) (max: Char) (chr: Char) : Bool
 = (Bool.and
-    (U60.to_bool #(>= chr min))
-    (U60.to_bool #(<= chr max))
+    (U60.to_bool (>= chr min))
+    (U60.to_bool (<= chr max))
  )
--- a/book/Char.is_blank.kind2
+++ b/book/Char.is_blank.kind2
@ -1,2 +1,2 @@
 Char.is_blank (a: Char) : Bool =
-  (Bool.or (Char.equal a #10) (Char.equal a #32))
+  (Bool.or (Char.equal a 10) (Char.equal a 32))
--- a/book/Char.is_decimal.kind2
+++ b/book/Char.is_decimal.kind2
@ -1,2 +1,2 @@
 Char.is_decimal (a: Char) : Bool =
-  (Char.is_between #48 #57 a)
+  (Char.is_between 48 57 a)
--- a/book/Char.is_name.kind2
+++ b/book/Char.is_name.kind2
@ -2,16 +2,16 @@ Char.is_name
 : ∀(a: Char) Bool
 = λa
  (Bool.or
-    (Char.is_between #97 #122 a)
+    (Char.is_between 97 122 a)
    (Bool.or
-      (Char.is_between #65 #90 a)
+      (Char.is_between 65 90 a)
      (Bool.or
-        (Char.is_between #48 #57 a)
+        (Char.is_between 48 57 a)
        (Bool.or
-          (Char.equal #95 a)
+          (Char.equal 95 a)
          (Bool.or
-            (Char.equal #46 a)
-            (Bool.or (Char.equal #45 a) Bool.false)
+            (Char.equal 46 a)
+            (Bool.or (Char.equal 45 a) Bool.false)
          )
        )
      )
--- a/book/Char.is_newline.kind2
+++ b/book/Char.is_newline.kind2
@ -1,3 +1,3 @@
 Char.is_newline
 : ∀(a: Char) Bool
-= λa (Char.equal a #10)
+= λa (Char.equal a 10)
--- a/book/Char.is_oper.kind2
+++ b/book/Char.is_oper.kind2
@ -2,30 +2,30 @@ Char.is_oper
 : ∀(a: Char) Bool
 = λa
  (Bool.or
-    (Char.equal #43 a)
+    (Char.equal 43 a)
    (Bool.or
-      (Char.equal #45 a)
+      (Char.equal 45 a)
      (Bool.or
-        (Char.equal #42 a)
+        (Char.equal 42 a)
        (Bool.or
-          (Char.equal #47 a)
+          (Char.equal 47 a)
          (Bool.or
-            (Char.equal #37 a)
+            (Char.equal 37 a)
            (Bool.or
-              (Char.equal #60 a)
+              (Char.equal 60 a)
              (Bool.or
-                (Char.equal #62 a)
+                (Char.equal 62 a)
                (Bool.or
-                  (Char.equal #61 a)
+                  (Char.equal 61 a)
                  (Bool.or
-                    (Char.equal #38 a)
+                    (Char.equal 38 a)
                    (Bool.or
-                      (Char.equal #124 a)
+                      (Char.equal 124 a)
                      (Bool.or
-                        (Char.equal #94 a)
+                        (Char.equal 94 a)
                        (Bool.or
-                          (Char.equal #33 a)
-                          (Bool.or (Char.equal #126 a) Bool.false)
+                          (Char.equal 33 a)
+                          (Bool.or (Char.equal 126 a) Bool.false)
                        )
                      )
                    )
--- a/book/Char.is_slash.kind2
+++ b/book/Char.is_slash.kind2
@ -1,3 +1,3 @@
 Char.is_slash
 : ∀(a: Char) Bool
-= λa (Char.equal a #47)
+= λa (Char.equal a 47)
--- a/book/Char.kind2
+++ b/book/Char.kind2
@ -1,3 +1,3 @@
 Char
 : *
-= #U60
+= U60
--- a/book/Char.slash.kind2
+++ b/book/Char.slash.kind2
@ -1,3 +1,3 @@
 Char.slash
 : Char
-= #47
+= 47
--- a/book/Equal.refl.kind2
+++ b/book/Equal.refl.kind2
@ -1,4 +1,4 @@
 Equal.refl
 : ∀(A: *) ∀(x: A) (Equal A x x)
 = λA λx
-  ~λP λp p
+  ~ λP λrefl (refl x)
--- a/book/IO.bind.kind2
+++ b/book/IO.bind.kind2
@ -18,4 +18,4 @@ IO.bind
      λx (IO.bind A B (then Unit.one) b)
    )
  use done = λterm λb (b term)
-  (~a P print load save done b)
+  (~a P print load save done b)
--- a/book/IO.done.kind2
+++ b/book/IO.done.kind2
@ -1,3 +1,3 @@
 IO.done
 : ∀(A: *) ∀(term: A) (IO A)
-= λA λterm ~λP λprint λload λsave λdone (done term)
+= λA λterm ~λP λprint λload λsave λdone (done term)
--- a/book/IO.kind2
+++ b/book/IO.kind2
@ -3,19 +3,8 @@ IO
 = λA
  $(self: (IO A))
  ∀(P: ∀(x: (IO A)) *)
-  ∀(print: 
-    ∀(text: String) ∀(then: ∀(x: Unit) (IO A))
-    (P (IO.print A text then))
-  )
-  ∀(load: 
-    ∀(file: String) ∀(then: ∀(x: String) (IO A))
-    (P (IO.load A file then))
-  )
-  ∀(save: 
-    ∀(file: String)
-    ∀(data: String)
-    ∀(then: ∀(x: Unit) (IO A))
-    (P (IO.save A file data then))
-  )
+  ∀(print: ∀(text: String) ∀(then: ∀(x: Unit) (IO A)) (P (IO.print A text then)))
+  ∀(load: ∀(file: String) ∀(then: ∀(x: String) (IO A)) (P (IO.load A file then)))
+  ∀(save: ∀(file: String) ∀(text: String) ∀(then: ∀(x: Unit) (IO A)) (P (IO.save A file text then)))
  ∀(done: ∀(term: A) (P (IO.done A term)))
-  (P self)
+  (P self)
--- a/book/IO.load.do.kind2
+++ b/book/IO.load.do.kind2
@ -1,3 +1,3 @@
 IO.load.do
 : ∀(file: String) (IO String)
-= λfile (IO.load String file λx (IO.done String x))
+= λfile (IO.load String file λx (IO.done String x))
--- a/book/IO.load.kind2
+++ b/book/IO.load.kind2
@ -4,4 +4,4 @@ IO.load
  ∀(then: ∀(x: String) (IO A))
  (IO A)
 = λA λfile λthen
-  ~λP λprint λload λsave λdone (load file then)
+  ~λP λprint λload λsave λdone (load file then)
--- a/book/IO.print.do.kind2
+++ b/book/IO.print.do.kind2
@ -1,3 +1,3 @@
 IO.print.do
 : ∀(text: String) (IO Unit)
-= λtext (IO.print Unit text λx (IO.done Unit x))
+= λtext (IO.print Unit text λx (IO.done Unit x))
--- a/book/IO.print.kind2
+++ b/book/IO.print.kind2
@ -2,4 +2,4 @@ IO.print
 : ∀(A: *) ∀(text: String) ∀(then: ∀(x: Unit) (IO A))
  (IO A)
 = λA λtext λthen
-  ~λP λprint λload λsave λdone (print text then)
+  ~λP λprint λload λsave λdone (print text then)
--- a/book/IO.run.kind2
+++ b/book/IO.run.kind2
@ -6,7 +6,7 @@ IO.run
    (HVM.print (IO A) text (IO.run A (then Unit.one)))
  use load = λfile λthen
    (HVM.load (IO A) file λs (IO.run A (then s)))
-  use save = λfile λdata λthen
-    (HVM.save (IO A) file data (IO.run A (then Unit.one)))
+  use save = λfile λtext λthen
+    (HVM.save (IO A) file text (IO.run A (then Unit.one)))
  use done = λterm (IO.done A term)
-  (~x P print load save done)
+  (~x P print load save done)
--- a/book/IO.save.do.kind2
+++ b/book/IO.save.do.kind2
@ -1,4 +1,4 @@
 IO.save.do
-: ∀(file: String) ∀(data: String) (IO Unit)
-= λfile λdata
-  (IO.save Unit file data λx (IO.done Unit x))
+: ∀(file: String) ∀(text: String) (IO Unit)
+= λfile λtext
+  (IO.save Unit file text λx (IO.done Unit x))
--- a/book/IO.save.kind2
+++ b/book/IO.save.kind2
@ -1,8 +1,8 @@
 IO.save
 : ∀(A: *)
  ∀(file: String)
-  ∀(data: String)
+  ∀(text: String)
  ∀(then: ∀(x: Unit) (IO A))
  (IO A)
-= λA λfile λdata λthen
-  ~λP λprint λload λsave λdone (save file data then)
+= λA λfile λtext λthen
+  ~λP λprint λload λsave λdone (save file text then)
--- a/book/Kind.API.to_hvm.kind2
+++ b/book/Kind.API.to_hvm.kind2
@ -1,18 +0,0 @@
-Kind.API.to_hvm
-: ∀(name: String) (IO Unit)
-= λname
-  (IO.run
-    Unit
-    (IO.bind
-      Kind.Book
-      Unit
-      (Kind.load.code name)
-      λbook
-      (IO.bind
-        Unit
-        Unit
-        (IO.print.do (Kind.Book.to_hvm book))
-        λx (IO.done Unit Unit.one)
-      )
-    )
-  )
--- a/book/Kind.Book.parse.kind2
+++ b/book/Kind.Book.parse.kind2
@ -4,4 +4,4 @@ Kind.Book.parse
  use P = λx Kind.Book
  use done = λcode λbook book
  use fail = λerror (String.Map.new Kind.Term)
-  (~(Kind.Book.parser code) P done fail)
+  (~(Kind.Book.parser code) P done fail)
--- a/book/Kind.Book.parser.kind2
+++ b/book/Kind.Book.parser.kind2
@ -91,4 +91,4 @@ Kind.Book.parser
        )
      )
    (~is_eof P true false)
-  )
+  )
--- a/book/Kind.Term.kind2
+++ b/book/Kind.Term.kind2
@ -37,7 +37,7 @@ Kind.Term
  )
  ∀(set: (P Kind.set))
  ∀(u60: (P Kind.u60))
-  ∀(num: ∀(val: #U60) (P (Kind.num val)))
+  ∀(num: ∀(val: U60) (P (Kind.num val)))
  ∀(op2: 
    ∀(opr: Kind.Oper) ∀(fst: Kind.Term) ∀(snd: Kind.Term)
    (P (Kind.op2 opr fst snd))
--- a/book/Kind.Term.parse.kind2
+++ b/book/Kind.Term.parse.kind2
@ -4,4 +4,4 @@ Kind.Term.parse
  use P = λx Kind.Term
  use done = λcode λterm (term (List.nil Kind.Binder))
  use fail = λerror (Kind.hol "error" (List.nil Kind.Term))
-  (~(Kind.Term.parser code) P done fail)
+  (~(Kind.Term.parser code) P done fail)
--- a/book/Kind.Term.parser.all.kind2
+++ b/book/Kind.Term.parser.all.kind2
@ -46,4 +46,4 @@ Kind.Term.parser.all
        )
      )
    )
-  )
+  )
--- a/book/Kind.Term.parser.chr.kind2
+++ b/book/Kind.Term.parser.chr.kind2
@ -8,7 +8,7 @@ Kind.Term.parser.chr
      (Parser.text "'")
      λ_
      (Kind.Term.parser.bind
-        #U60
+        U60
        Parser.char
        λchr
        (Kind.Term.parser.bind
--- a/book/Kind.Term.parser.kind2
+++ b/book/Kind.Term.parser.kind2
@ -47,4 +47,4 @@ Kind.Term.parser
        )
      )
    )
-  )
+  )
--- a/book/Kind.Term.parser.mat.kind2
+++ b/book/Kind.Term.parser.mat.kind2
@ -2,10 +2,10 @@ Kind.Term.parser.mat
 : (Parser.Guard Kind.PreTerm)
 = (Parser.Guard.text
    Kind.PreTerm
-    "#match "
+    "switch "
    (Kind.Term.parser.bind
      Unit
-      (Parser.text "#match ")
+      (Parser.text "switch ")
      λ_
      (Kind.Term.parser.bind
        String
@ -25,7 +25,7 @@ Kind.Term.parser.mat
              λ_
              (Kind.Term.parser.bind
                Unit
-                (Parser.text "#0")
+                (Parser.text "0")
                λ_
                (Kind.Term.parser.bind
                  Unit
@ -37,7 +37,7 @@ Kind.Term.parser.mat
                    λz
                    (Kind.Term.parser.bind
                      Unit
-                      (Parser.text "#+")
+                      (Parser.text "+")
                      λ_
                      (Kind.Term.parser.bind
                        Unit
--- a/book/Kind.Term.parser.num.kind2
+++ b/book/Kind.Term.parser.num.kind2
@ -2,13 +2,13 @@ Kind.Term.parser.num
 : (Parser.Guard Kind.PreTerm)
 = (Parser.Guard.text
    Kind.PreTerm
-    "#"
+    ""
    (Kind.Term.parser.bind
      Unit
-      (Parser.text "#")
+      (Parser.text "")
      λ_
      (Kind.Term.parser.bind
-        #U60
+        U60
        U60.parser.decimal
        λnum (Kind.Term.parser.pure λscp (Kind.num num))
      )
--- a/book/Kind.Term.parser.op2.kind2
+++ b/book/Kind.Term.parser.op2.kind2
@ -2,10 +2,10 @@ Kind.Term.parser.op2
 : (Parser.Guard Kind.PreTerm)
 = (Parser.Guard.text
    Kind.PreTerm
-    "#("
+    "("
    (Kind.Term.parser.bind
      _
-      (Parser.text "#(")
+      (Parser.text "(")
      λ_
      (Kind.Term.parser.bind
        _
--- a/book/Kind.Term.parser.u60.kind2
+++ b/book/Kind.Term.parser.u60.kind2
@ -2,10 +2,10 @@ Kind.Term.parser.u60
 : (Parser.Guard Kind.PreTerm)
 = (Parser.Guard.text
    Kind.PreTerm
-    "#U60"
+    "U60"
    (Kind.Term.parser.bind
      Unit
-      (Parser.text "#U60")
+      (Parser.text "U60")
      λ_ (Kind.Term.parser.pure λscp Kind.u60)
    )
  )
--- a/book/Kind.Term.show.go.kind2
+++ b/book/Kind.Term.show.go.kind2
@ -104,11 +104,11 @@ Kind.Term.show.go
      )
    )
  use set = λnil (Kind.Text.show.go "*" nil)
-  use u60 = λnil (Kind.Text.show.go "#U60" nil)
-  use num = λval λnil (Kind.Text.show.go "#" (U60.show.go val nil))
+  use u60 = λnil (Kind.Text.show.go "U60" nil)
+  use num = λval λnil (Kind.Text.show.go "" (U60.show.go val nil))
  use op2 = λopr λfst λsnd λnil
    (Kind.Text.show.go
-      "#("
+      "("
      (Kind.Oper.show.go
        opr
        (Kind.Text.show.go
@ -126,7 +126,7 @@ Kind.Term.show.go
    )
  use mat = λnam λx λz λs λp λnil
    (Kind.Text.show.go
-      "#match "
+      "switch "
      (Kind.Text.show.go
        nam
        (Kind.Text.show.go
@ -135,12 +135,12 @@ Kind.Term.show.go
            x
            dep
            (Kind.Text.show.go
-              " { #0: "
+              " { 0: "
              (Kind.Term.show.go
                z
                dep
                (Kind.Text.show.go
-                  "; #+: "
+                  "; +: "
                  (Kind.Term.show.go
                    (s (Kind.var (String.concat nam "-1") dep))
                    (Nat.succ dep)
--- a/book/Kind.if.num.kind2
+++ b/book/Kind.if.num.kind2
@ -1,12 +1,12 @@
 Kind.if.num
 : ∀(term: Kind.Term)
  ∀(P: *)
-  ∀(Y: ∀(val: #U60) P)
+  ∀(Y: ∀(val: U60) P)
  ∀(N: ∀(val: Kind.Term) P)
  P
 = λterm λP λY λN
  use P = λx
-    ∀(Y: ∀(val: #U60) P) ∀(N: ∀(val: Kind.Term) P) P
+    ∀(Y: ∀(val: U60) P) ∀(N: ∀(val: Kind.Term) P) P
  use all = λnam λinp λbod λY λN (N (Kind.all nam inp bod))
  use lam = λnam λbod λY λN (N (Kind.lam nam bod))
  use app = λfun λarg λY λN (N (Kind.app fun arg))
--- a/book/Kind.infer.kind2
+++ b/book/Kind.infer.kind2
@ -83,7 +83,7 @@ Kind.infer
        )
        λp_typ
        (bind
-          (Kind.check z (p (Kind.num #0)) dep)
+          (Kind.check z (p (Kind.num 0)) dep)
          λz_typ
          (bind
            (Kind.check
@ -96,7 +96,7 @@ Kind.infer
              (p
                (Kind.op2
                  Kind.Oper.add
-                  (Kind.num #1)
+                  (Kind.num 1)
                  (Kind.var (String.concat nam "-1") dep)
                )
              )
--- a/book/Kind.load.code.kind2
+++ b/book/Kind.load.code.kind2
@ -5,4 +5,4 @@ Kind.load.code
    Kind.Book
    (String.concat name ".kind2")
    λdata (IO.done Kind.Book (Kind.Book.parse data))
-  )
+  )
--- a/book/Kind.num.kind2
+++ b/book/Kind.num.kind2
@ -1,5 +1,5 @@
 Kind.num
-: ∀(val: #U60) Kind.Term
+: ∀(val: U60) Kind.Term
 = λval
  ~λP λall λlam λapp λann λslf λins λref λdef λset λu60 λnum λop2 λmat λtxt λhol λvar
  (num val)
--- a/book/Kind.reduce.mat.kind2
+++ b/book/Kind.reduce.mat.kind2
@ -10,9 +10,9 @@ Kind.reduce.mat
  use P = ∀(z: Kind.Term) ∀(s: ∀(x: Kind.Term) Kind.Term)
    Kind.Term
  use Y = λx.val
-    #match x = x.val {
-      #0: λz λs (Kind.reduce maj z)
-      #+: λz λs (Kind.reduce maj (s (Kind.num x-1))) 
+    switch x = x.val {
+      0: λz λs (Kind.reduce maj z)
+      +: λz λs (Kind.reduce maj (s (Kind.num x-1))) 
    }: ∀(z: Kind.Term) ∀(s: ∀(x: Kind.Term) Kind.Term)
    Kind.Term
  use N = λx λz λs (Kind.mat nam x z s p)
--- a/book/Kind.reduce.op2.kind2
+++ b/book/Kind.reduce.op2.kind2
@ -4,25 +4,25 @@ Kind.reduce.op2
 = λopr λfst λsnd
  use P = ∀(snd: Kind.Term) Kind.Term
  use Y = λfst_val λsnd
-    use P = ∀(fst_val: #U60) Kind.Term
+    use P = ∀(fst_val: U60) Kind.Term
    use Y = λsnd_val λfst_val
-      use P = λx ∀(fst_val: #U60) ∀(snd_val: #U60) Kind.Term
-      use add = λfst_val λsnd_val (Kind.num #(+ fst_val snd_val))
-      use mul = λfst_val λsnd_val (Kind.num #(* fst_val snd_val))
-      use sub = λfst_val λsnd_val (Kind.num #(- fst_val snd_val))
-      use div = λfst_val λsnd_val (Kind.num #(/ fst_val snd_val))
-      use mod = λfst_val λsnd_val (Kind.num #(% fst_val snd_val))
-      use eq = λfst_val λsnd_val (Kind.num #(== fst_val snd_val))
-      use ne = λfst_val λsnd_val (Kind.num #(!= fst_val snd_val))
-      use lt = λfst_val λsnd_val (Kind.num #(< fst_val snd_val))
-      use gt = λfst_val λsnd_val (Kind.num #(> fst_val snd_val))
-      use lte = λfst_val λsnd_val (Kind.num #(<= fst_val snd_val))
-      use gte = λfst_val λsnd_val (Kind.num #(>= fst_val snd_val))
-      use and = λfst_val λsnd_val (Kind.num #(& fst_val snd_val))
-      use or = λfst_val λsnd_val (Kind.num #(| fst_val snd_val))
-      use xor = λfst_val λsnd_val (Kind.num #(^ fst_val snd_val))
-      use lsh = λfst_val λsnd_val (Kind.num #(<< fst_val snd_val))
-      use rsh = λfst_val λsnd_val (Kind.num #(>> fst_val snd_val))
+      use P = λx ∀(fst_val: U60) ∀(snd_val: U60) Kind.Term
+      use add = λfst_val λsnd_val (Kind.num (+ fst_val snd_val))
+      use mul = λfst_val λsnd_val (Kind.num (* fst_val snd_val))
+      use sub = λfst_val λsnd_val (Kind.num (- fst_val snd_val))
+      use div = λfst_val λsnd_val (Kind.num (/ fst_val snd_val))
+      use mod = λfst_val λsnd_val (Kind.num (% fst_val snd_val))
+      use eq = λfst_val λsnd_val (Kind.num (== fst_val snd_val))
+      use ne = λfst_val λsnd_val (Kind.num (!= fst_val snd_val))
+      use lt = λfst_val λsnd_val (Kind.num (< fst_val snd_val))
+      use gt = λfst_val λsnd_val (Kind.num (> fst_val snd_val))
+      use lte = λfst_val λsnd_val (Kind.num (<= fst_val snd_val))
+      use gte = λfst_val λsnd_val (Kind.num (>= fst_val snd_val))
+      use and = λfst_val λsnd_val (Kind.num (& fst_val snd_val))
+      use or = λfst_val λsnd_val (Kind.num (| fst_val snd_val))
+      use xor = λfst_val λsnd_val (Kind.num (^ fst_val snd_val))
+      use lsh = λfst_val λsnd_val (Kind.num (<< fst_val snd_val))
+      use rsh = λfst_val λsnd_val (Kind.num (>> fst_val snd_val))
      (~opr
        P
        add
--- a/book/Nat.lemma.bft.kind2
+++ b/book/Nat.lemma.bft.kind2
@ -8,26 +8,3 @@ bft (n: Nat) : {(half (double n)) = n} =
      prf
    zero: {=}
  }
-
-//#found{a
-  //(((Equal (_)) (Nat.succ {n.pred: Nat})) (Nat.half (Nat.double {(Nat.succ {n.pred: Nat}): Nat})))
-  //[
-    //{n: Nat}
-    //λn (((Equal (_)) n) (Nat.half (Nat.double {n: Nat})))
-    //{n.pred: Nat}
-    //{ind: (((Equal (_)) (Nat.half (Nat.double n.pred))) n.pred)}
-  //]}
-
-  //(~n
-    //λx (Equal Nat (Nat.half (Nat.double x)) x)
-    //λn
-    //(Equal.apply
-      //Nat
-      //Nat
-      //Nat.succ
-      //(Nat.half (Nat.double n))
-      //n
-      //(Nat.lemma.bft n)
-    //)
-    //λP λa a
-  //)
--- a/book/Parser.text.kind2
+++ b/book/Parser.text.kind2
@ -20,4 +20,4 @@ Parser.text
        (Parser.fail Unit "error")
      )
    )
-  )
+  )
--- a/book/QBool.false.kind2
+++ b/book/QBool.false.kind2
@ -1,3 +1,3 @@
 QBool.false
 : QBool
-= ~λP ~λS λp (p #1 λx x)
+= ~λP ~λS λp (p 1 λx x)
--- a/book/QBool.kind2
+++ b/book/QBool.kind2
@ -3,16 +3,16 @@ QBool
 = $(self: QBool)
  ∀(P: ∀(x: QBool) *)
  (Sigma
-    #U60
+    U60
    λt
    ∀(x: 
-      #match t = t {
-        #0: (P QBool.true)
-        #+: #match t = t-1 {
-          #0: (P QBool.false)
-          #+: ∀(x: Empty) * 
+      switch t = t {
+        0: (P QBool.true)
+        +: switch t = t-1 {
+          0: (P QBool.false)
+          +: ∀(x: Empty) * 
        }: * 
      }: *
    )
    (P self)
-  )
+  )
--- a/book/QBool.match.kind2
+++ b/book/QBool.match.kind2
@ -8,17 +8,17 @@ QBool.match
  (~(~a P)
    λx (P a)
    λtag
-    #match tag = tag {
-      #0: λx (x t)
-      #+: λx
-      (#match tag_1 = tag-1 {
-        #0: λx (x f)
-        #+: λx (x λe (Empty.absurd e *)) 
+    switch tag = tag {
+      0: λx (x t)
+      +: λx
+      (switch tag_1 = tag-1 {
+        0: λx (x f)
+        +: λx (x λe (Empty.absurd e *)) 
      }: ∀(x: 
        ∀(x: 
-          #match tag_1 = tag_1 {
-            #0: (P QBool.false)
-            #+: ∀(x: Empty) * 
+          switch tag_1 = tag_1 {
+            0: (P QBool.false)
+            +: ∀(x: Empty) * 
          }: *
        )
        (P a)
@ -28,15 +28,15 @@ QBool.match
      ) 
    }: ∀(x: 
      ∀(x: 
-        #match tag = tag {
-          #0: (P QBool.true)
-          #+: #match tag_1 = tag-1 {
-            #0: (P QBool.false)
-            #+: ∀(x: Empty) * 
+        switch tag = tag {
+          0: (P QBool.true)
+          +: switch tag_1 = tag-1 {
+            0: (P QBool.false)
+            +: ∀(x: Empty) * 
          }: * 
        }: *
      )
      (P a)
    )
    (P a)
-  )
+  )
--- a/book/QBool.true.kind2
+++ b/book/QBool.true.kind2
@ -1,3 +1,3 @@
 QBool.true
 : QBool
-= ~λP ~λS λp (p #0 λx x)
+= ~λP ~λS λp (p 0 λx x)
--- a/book/QBool2.false.kind2
+++ b/book/QBool2.false.kind2
@ -1,3 +1,3 @@
 QBool2.false
 : QBool2
-= ~λP λnew (new #1)
+= ~λP λnew (new 1)
--- a/book/QBool2.kind2
+++ b/book/QBool2.kind2
@ -3,12 +3,12 @@ QBool2
 = $(self: QBool2)
  ∀(P: ∀(x: QBool2) *)
  ∀(new: 
-    ∀(tag: #U60)
-    #match tag = tag {
-      #0: (P QBool2.true)
-      #+: #match tag_1 = tag-1 {
-        #0: (P QBool2.false)
-        #+: ∀(e: Empty) * 
+    ∀(tag: U60)
+    switch tag = tag {
+      0: (P QBool2.true)
+      +: switch tag_1 = tag-1 {
+        0: (P QBool2.false)
+        +: ∀(e: Empty) * 
      }: * 
    }: *
  )
--- a/book/QBool2.match.kind2
+++ b/book/QBool2.match.kind2
@ -8,20 +8,20 @@ QBool2.match
  (~a
    P
    λtag
-    #match tag = tag {
-      #0: t
-      #+: #match tag_1 = tag-1 {
-        #0: f
-        #+: λe (~e λx *) 
-      }: #match tag_1 = tag_1 {
-        #0: (P QBool2.false)
-        #+: ∀(e: Empty) * 
+    switch tag = tag {
+      0: t
+      +: switch tag_1 = tag-1 {
+        0: f
+        +: λe (~e λx *) 
+      }: switch tag_1 = tag_1 {
+        0: (P QBool2.false)
+        +: ∀(e: Empty) * 
      }: * 
-    }: #match tag = tag {
-      #0: (P QBool2.true)
-      #+: #match tag_1 = tag-1 {
-        #0: (P QBool2.false)
-        #+: ∀(e: Empty) * 
+    }: switch tag = tag {
+      0: (P QBool2.true)
+      +: switch tag_1 = tag-1 {
+        0: (P QBool2.false)
+        +: ∀(e: Empty) * 
      }: * 
    }: *
-  )
+  )
--- a/book/QBool2.true.kind2
+++ b/book/QBool2.true.kind2
@ -1,3 +1,3 @@
 QBool2.true
 : QBool2
-= ~λP λnew (new #0)
+= ~λP λnew (new 0)
--- a/book/QUnit.kind2
+++ b/book/QUnit.kind2
@ -3,10 +3,10 @@ QUnit
 = $(self: QUnit)
  ∀(P: ∀(x: QUnit) *)
  (Sigma
-    #U60
+    U60
    λtag
-    #match tag = tag {
-      #0: ∀(one: (P QUnit.one)) (P self)
-      #+: Empty 
+    switch tag = tag {
+      0: ∀(one: (P QUnit.one)) (P self)
+      +: Empty 
    }: *
  )
--- a/book/String.indent.kind2
+++ b/book/String.indent.kind2
@ -4,8 +4,8 @@ String.indent
  use P = λx String
  use succ = λtab.pred
    (String.cons
-      #32
-      (String.cons #32 (String.indent tab.pred))
+      32
+      (String.cons 32 (String.indent tab.pred))
    )
  use zero = String.nil
  (~tab P succ zero)
--- a/book/String.length.kind2
+++ b/book/String.length.kind2
@ -1,3 +1,3 @@
 String.length
 : ∀(a: String) Nat
-= λa (List.length Char a)
+= λa (List.length Char a)
--- a/book/String.newline.kind2
+++ b/book/String.newline.kind2
@ -1,3 +1,3 @@
 String.newline
 : String
-= (String.cons #10 String.nil)
+= (String.cons 10 String.nil)
--- a/book/String.quote.kind2
+++ b/book/String.quote.kind2
@ -1,3 +1,3 @@
 String.quote
 : String
-= (String.cons #34 String.nil)
+= (String.cons 34 String.nil)
--- a/book/U60.Map.kind2
+++ b/book/U60.Map.kind2
@ -1,3 +1,3 @@
 U60.Map
 : ∀(V: *) *
-= λV (BBT #U60 V)
+= λV (BBT U60 V)
--- a/book/U60.abs_diff.kind2
+++ b/book/U60.abs_diff.kind2
@ -1,7 +1,7 @@
 U60.abs_diff
-: ∀(a: #U60) ∀(b: #U60) #U60
+: ∀(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)
+  use P = λx U60
+  use true = (- b a)
+  use false = (- a b)
+  (~(U60.to_bool (< a b)) P true false)
--- a/book/U60.cmp.kind2
+++ b/book/U60.cmp.kind2
@ -1,9 +1,9 @@
 U60.cmp
-: ∀(a: #U60) ∀(b: #U60) Cmp
+: ∀(a: U60) ∀(b: U60) Cmp
 = λa λb
  (U60.if
-    #(== a b)
+    (== a b)
    Cmp
-    (U60.if #(< a b) Cmp Cmp.gtn Cmp.ltn)
+    (U60.if (< a b) Cmp Cmp.gtn Cmp.ltn)
    Cmp.eql
  )
--- a/book/U60.equal.kind2
+++ b/book/U60.equal.kind2
@ -1,7 +1,7 @@
 U60.equal
-: ∀(a: #U60) ∀(b: #U60) Bool
+: ∀(a: U60) ∀(b: U60) Bool
 = λa λb
-  #match x = #(== a b) {
-    #0: Bool.false
-    #+: Bool.true 
+  switch x = (== a b) {
+    0: Bool.false
+    +: Bool.true 
  }: Bool
--- a/book/U60.from_nat.kind2
+++ b/book/U60.from_nat.kind2
@ -1,7 +1,7 @@
 U60.from_nat
-: ∀(n: Nat) #U60
+: ∀(n: Nat) U60
 = λn
-  use P = λx #U60
-  use succ = λn.pred #(+ #1 (U60.from_nat n.pred))
-  use zero = #0
+  use P = λx U60
+  use succ = λn.pred (+ 1 (U60.from_nat n.pred))
+  use zero = 0
  (~n P succ zero)
--- a/book/U60.if.kind2
+++ b/book/U60.if.kind2
@ -1,3 +1,3 @@
 U60.if
-: ∀(x: #U60) ∀(P: *) ∀(t: P) ∀(f: P) P
-= λx λP λt λf #match x = x { #0: t #+: f }: P
+: ∀(x: U60) ∀(P: *) ∀(t: P) ∀(f: P) P
+= λx λP λt λf switch x = x { 0: t +: f }: P
--- a/book/U60.match.kind2
+++ b/book/U60.match.kind2
@ -1,8 +1,8 @@
-U60.match
-: ∀(x: #U60)
-  ∀(P: ∀(x: #U60) *)
-  ∀(s: ∀(x: #U60) (P #(+ #1 x)))
-  ∀(z: (P #0))
+U60.switch
+: ∀(x: U60)
+  ∀(P: ∀(x: U60) *)
+  ∀(s: ∀(x: U60) (P (+ 1 x)))
+  ∀(z: (P 0))
  (P x)
 = λx λP λs λz
-  #match self = x { #0: z #+: (s self-1) }: (P self)
+  switch self = x { 0: z +: (s self-1) }: (P self)
--- a/book/U60.max.kind2
+++ b/book/U60.max.kind2
@ -1,3 +1,3 @@
 U60.max
-: ∀(a: #U60) ∀(b: #U60) #U60
-= λa λb (~(U60.to_bool #(> a b)) λx #U60 a b)
+: ∀(a: U60) ∀(b: U60) U60
+= λa λb (~(U60.to_bool (> a b)) λx U60 a b)
--- a/book/U60.min.kind2
+++ b/book/U60.min.kind2
@ -1,3 +1,3 @@
 U60.min
-: ∀(a: #U60) ∀(b: #U60) #U60
-= λa λb (~(U60.to_bool #(< a b)) λx #U60 a b)
+: ∀(a: U60) ∀(b: U60) U60
+= λa λb (~(U60.to_bool (< a b)) λx U60 a b)
--- a/book/U60.name.go.kind2
+++ b/book/U60.name.go.kind2
@ -1,11 +1,11 @@
 U60.name.go
-: ∀(n: #U60) String.Concatenator
+: ∀(n: U60) String.Concatenator
 = λn
-  #match n = n {
-    #0: λnil nil
-    #+: λnil
+  switch n = n {
+    0: λnil nil
+    +: λnil
    (String.cons
-      #(+ #97 #(% n-1 #26))
-      (U60.name.go #(/ n-1 #26) nil)
+      (+ 97 (% n-1 26))
+      (U60.name.go (/ n-1 26) nil)
    ) 
  }: String.Concatenator
--- a/book/U60.name.kind2
+++ b/book/U60.name.kind2
@ -1,3 +1,3 @@
 U60.name
-: ∀(n: #U60) String
-= λn (String.Concatenator.build (U60.name.go #(+ n #1)))
+: ∀(n: U60) String
+= λn (String.Concatenator.build (U60.name.go (+ n 1)))
--- a/book/U60.parser.decimal.kind2
+++ b/book/U60.parser.decimal.kind2
@ -1,19 +1,19 @@
 U60.parser.decimal
-: (Parser #U60)
+: (Parser U60)
 = (Parser.bind
    String
-    #U60
+    U60
    Parser.decimal
    λchars
    (Parser.pure
-      #U60
+      U60
      (List.fold
        Char
        chars
-        ∀(r: #U60) #U60
-        λh λt λr (t #(+ #(- h #48) #(* r #10)))
+        ∀(r: U60) U60
+        λh λt λr (t (+ (- h 48) (* r 10)))
        λr r
-        #0
+        0
      )
    )
  )
--- a/book/U60.show.go.kind2
+++ b/book/U60.show.go.kind2
@ -1,11 +1,11 @@
 U60.show.go
-: ∀(n: #U60) String.Concatenator
+: ∀(n: U60) String.Concatenator
 = λn
-  #match x = #(< n #10) {
-    #0: λnil
+  switch x = (< n 10) {
+    0: λnil
    (U60.show.go
-      #(/ n #10)
-      (String.cons #(+ #48 #(% n #10)) nil)
+      (/ n 10)
+      (String.cons (+ 48 (% n 10)) nil)
    )
-    #+: λnil (String.cons #(+ #48 n) nil) 
+    +: λnil (String.cons (+ 48 n) nil) 
  }: String.Concatenator
--- a/book/U60.show.kind2
+++ b/book/U60.show.kind2
@ -1,3 +1,3 @@
 U60.show
-: ∀(n: #U60) String
+: ∀(n: U60) String
 = λn (String.Concatenator.build (U60.show.go n))
--- a/book/U60.to_bool.kind2
+++ b/book/U60.to_bool.kind2
@ -1,3 +1,5 @@
-U60.to_bool
-: ∀(x: #U60) Bool
-= λx #match x = x { #0: Bool.false #+: Bool.true }: Bool
+U60.to_bool (x: U60) : Bool =
+  switch x {
+    0: Bool.false
+    +: Bool.true
+  }: Bool
--- a/book/Unit.match.kind2
+++ b/book/Unit.match.kind2
@ -1,4 +1,4 @@
-Unit.match
+Unit.switch
 : ∀(x: Unit) ∀(P: ∀(x: Unit) *) ∀(o: (P Unit.one))
  (P x)
 = λx λP λo (~x P o)
--- a/book/Vector.concat.kind2
+++ b/book/Vector.concat.kind2
@ -5,7 +5,7 @@ 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 {
+= switch xs {
    cons : (cons T (add xs.len ys_len) xs.head (concat T xs.len ys_len xs.tail ys))
    nil  : ys
  }
--- a/book/_err.txt
+++ b/book/_err.txt
@ -1,4 +1,4 @@
-QBool.match
+QBool.switch
 : ∀(a: QBool)
  ∀(P: ∀(x: QBool) *)
  ∀(t: (P QBool.true))
@ -8,17 +8,17 @@ QBool.match
  (~(~a P)
    λx (P a)
    λtag
-    #match tag = tag {
-      #0: λx (x t)
-      #+: λx
-      (#match tag_1 = tag-1 {
-        #0: λx (x f)
-        #+: λx (x λe (Empty.absurd e *)) 
+    switch tag = tag {
+      0: λx (x t)
+      +: λx
+      (switch tag_1 = tag-1 {
+        0: λx (x f)
+        +: λx (x λe (Empty.absurd e *)) 
      }: ∀(x: 
        ∀(x: 
-          #match tag_1 = tag_1 {
-            #0: (P QBool.false)
-            #+: ∀(x: Empty) * 
+          switch tag_1 = tag_1 {
+            0: (P QBool.false)
+            +: ∀(x: Empty) * 
          }: *
        )
        (P a)
@ -28,11 +28,11 @@ QBool.match
      ) 
    }: ∀(x: 
      ∀(x: 
-        #match tag = tag {
-          #0: (P QBool.true)
-          #+: #match tag_1 = tag-1 {
-            #0: (P QBool.false)
-            #+: ∀(x: Empty) * 
+        switch tag = tag {
+          0: (P QBool.true)
+          +: switch tag_1 = tag-1 {
+            0: (P QBool.false)
+            +: ∀(x: Empty) * 
          }: * 
        }: *
      )
@ -41,7 +41,7 @@ QBool.match
    (P a)
  )

-QBool2.match
+QBool2.switch
 : ∀(a: QBool2)
  ∀(P: ∀(x: QBool2) *)
  ∀(t: (P QBool2.true))
@ -51,20 +51,20 @@ QBool2.match
  (~a
    P
    λtag
-    #match tag = tag {
-      #0: t
-      #+: #match tag_1 = tag-1 {
-        #0: f
-        #+: λe (~e λx *) 
-      }: #match tag_1 = tag_1 {
-        #0: (P QBool2.false)
-        #+: ∀(e: Empty) * 
+    switch tag = tag {
+      0: t
+      +: switch tag_1 = tag-1 {
+        0: f
+        +: λe (~e λx *) 
+      }: switch tag_1 = tag_1 {
+        0: (P QBool2.false)
+        +: ∀(e: Empty) * 
      }: * 
-    }: #match tag = tag {
-      #0: (P QBool2.true)
-      #+: #match tag_1 = tag-1 {
-        #0: (P QBool2.false)
-        #+: ∀(e: Empty) * 
+    }: switch tag = tag {
+      0: (P QBool2.true)
+      +: switch tag_1 = tag-1 {
+        0: (P QBool2.false)
+        +: ∀(e: Empty) * 
      }: * 
    }: *
  )
--- a/book/_main.kind2
+++ b/book/_main.kind2
@ -5,16 +5,16 @@
 //use Nat.{succ,zero}

 _main : Nat =
-  (Nat.half (Nat.double 3))
+  #50
  

 //_main (a: Nat) (b: Nat) (e: (Equal A a b)) : (Equal A a b) =
-  //match a {
-    //succ: match b {
+  //switch a {
+    //succ: switch b {
      //succ: e
      //zero: e
    //}
-    //zero: match b {
+    //zero: switch b {
      //succ: e
      //zero: ?D
    //}
@ -35,12 +35,12 @@ _main : Nat =
  //): ∀(e2: (Equal A a b)) _} e)

 //_main (a: Nat) (b: Nat) (e: (Equal A a b)) : (Equal A a b) =
-  //match a {
-    //succ: match b {
+  //switch a {
+    //succ: switch b {
      //succ: ?A
      //zero: ?B
    //}
-    //zero: match b {
+    //zero: switch b {
      //succ: ?C
      //zero: ?D
    //}
@ -58,7 +58,7 @@ _main : Nat =
    //)
  //)

-//match x {
+//switch x {
 //}

 //_main
@ -130,12 +130,12 @@ _main : Nat =
  //)


-//match a {
-  //cons: match b {
+//switch a {
+  //cons: switch b {
    //cons: ... a.tail ...
    //nil: ... a.tail ...
  //}
-  //nil: match b {
+  //nil: switch b {
    //cons:
    //nil: 
  //}
--- a/book/test1.kind2
+++ b/book/test1.kind2
@ -1,3 +1,3 @@
 test1
-: ∀(x: #U60) #U60
-= λx #(+ #50 #12)
+: ∀(x: U60) U60
+= λx (+ 50 12)
--- a/book/test11.kind2
+++ b/book/test11.kind2
@ -1,3 +1,3 @@
 test11
 : String
-= #0
+= 0
--- a/book/test2.kind2
+++ b/book/test2.kind2
@ -1,13 +1,13 @@
 test2
-: (List #U60)
+: (List U60)
 = use xs = (List.cons
-      #U60
-      #0
-      (List.cons #U60 #1 (List.cons #U60 #2 (List.nil #U60)))
+      U60
+      0
+      (List.cons U60 1 (List.cons U60 2 (List.nil U60)))
    )
  use ys = (List.cons
-      #U60
-      #3
-      (List.cons #U60 #4 (List.cons #U60 #5 (List.nil #U60)))
+      U60
+      3
+      (List.cons U60 4 (List.cons U60 5 (List.nil U60)))
    )
-  (List.concat #U60 xs ys)
+  (List.concat U60 xs ys)
--- a/book/test3.kind2
+++ b/book/test3.kind2
@ -1,4 +1,4 @@
 test3
-: #U60
-= use a = {#42:#U60}
+: U60
+= use a = {42:U60}
  a
--- a/book/test8.kind2
+++ b/book/test8.kind2
@ -1,7 +1,7 @@
 test8
-: ∀(b: Bool) (~b λx(*) #U60 #U60)
+: ∀(b: Bool) (~b λx(*) U60 U60)
 = λb (~b _h ?A ?B)

 //test8
-//: #U60
-//= (U60.test #0)
+//: U60
+//= (U60.test 0)
--- a/book/test9.kind2
+++ b/book/test9.kind2
@ -1,3 +1,3 @@
 test9
 : String
-= (String.unpar #40 #41 "((foo))")
+= (String.unpar 40 41 "((foo))")
--- a/src/book/parse.rs
+++ b/src/book/parse.rs
@ -163,7 +163,7 @@ impl Term {
      return;
    }
    // Linearizes a numeric pattern match
-    if let Term::Mat { nam, z, s, .. } = self {
+    if let Term::Swi { nam, z, s, .. } = self {
      if args.len() >= 1 && args[0].0 == *nam {
        let (head, tail) = args.split_at(1);
        z.add_lams(tail.clone());
--- a/src/kind2.hs
+++ b/src/kind2.hs
@ -34,7 +34,7 @@ data Term
  | U60
  | Num Int
  | Op2 Oper Term Term
-  | Mat String Term Term (Term -> Term) (Term -> Term)
+  | Swi String Term Term (Term -> Term) (Term -> Term)
  | Hol String [Term]
  | Met Int [Term]
  | Var String Int
@ -239,7 +239,7 @@ termReduce fill lv (Ref nam val)     = termReduceRef fill lv nam (termReduce fil
 termReduce fill lv (Let nam val bod) = termReduce fill lv (bod val)
 termReduce fill lv (Use nam val bod) = termReduce fill lv (bod val)
 termReduce fill lv (Op2 opr fst snd) = termReduceOp2 fill lv opr (termReduce fill lv fst) (termReduce fill lv snd)
-termReduce fill lv (Mat nam x z s p) = termReduceMat fill lv nam (termReduce fill lv x) z s p
+termReduce fill lv (Swi nam x z s p) = termReduceSwi fill lv nam (termReduce fill lv x) z s p
 termReduce fill lv (Txt txt)         = termReduceTxt fill lv txt
 termReduce fill lv (Nat val)         = termReduceNat fill lv val
 termReduce fill lv (Src src val)     = termReduce fill lv val
@ -280,13 +280,13 @@ termReduceOp2 fill lv LTE (Num fst) (Num snd) = if fst <= snd then Num 1 else Nu
 termReduceOp2 fill lv GTE (Num fst) (Num snd) = if fst >= snd then Num 1 else Num 0
 termReduceOp2 fill lv opr fst snd             = Op2 opr fst snd

-termReduceMat :: Map Term -> Int -> String -> Term -> Term -> (Term -> Term) -> (Term -> Term) -> Term
-termReduceMat fill 2  nam (Ref _ x)           z s p = termReduceMat fill 2 nam x z s p
-termReduceMat fill 1  nam (Ref _ x)           z s p = termReduceMat fill 1 nam x z s p
-termReduceMat fill lv nam (Num 0)             z s p = termReduce fill lv z
-termReduceMat fill lv nam (Num n)             z s p = termReduce fill lv (s (Num (n - 1)))
-termReduceMat fill lv nam (Op2 ADD (Num 1) k) z s p = termReduce fill lv (s k)
-termReduceMat fill lv nam val                 z s p = Mat nam val z s p
+termReduceSwi :: Map Term -> Int -> String -> Term -> Term -> (Term -> Term) -> (Term -> Term) -> Term
+termReduceSwi fill 2  nam (Ref _ x)           z s p = termReduceSwi fill 2 nam x z s p
+termReduceSwi fill 1  nam (Ref _ x)           z s p = termReduceSwi fill 1 nam x z s p
+termReduceSwi fill lv nam (Num 0)             z s p = termReduce fill lv z
+termReduceSwi fill lv nam (Num n)             z s p = termReduce fill lv (s (Num (n - 1)))
+termReduceSwi fill lv nam (Op2 ADD (Num 1) k) z s p = termReduce fill lv (s k)
+termReduceSwi fill lv nam val                 z s p = Swi nam val z s p

 termReduceRef :: Map Term -> Int -> String -> Term -> Term
 termReduceRef fill 2  nam val = termReduce fill 2 val
@ -327,7 +327,7 @@ termNormal fill lv term dep = termNormalGo fill lv (termReduce fill lv term) dep
  termNormalGo fill lv U60               dep = U60
  termNormalGo fill lv (Num val)         dep = Num val
  termNormalGo fill lv (Op2 opr fst snd) dep = Op2 opr (termNormal fill lv fst dep) (termNormal fill lv snd dep)
-  termNormalGo fill lv (Mat nam x z s p) dep = Mat nam (termNormal fill lv x dep) (termNormal fill lv z dep) (\k -> termNormal fill lv (s (Var (stringConcat nam "-1") dep)) dep) (\k -> termNormal fill lv (p (Var nam dep)) dep)
+  termNormalGo fill lv (Swi nam x z s p) dep = Swi nam (termNormal fill lv x dep) (termNormal fill lv z dep) (\k -> termNormal fill lv (s (Var (stringConcat nam "-1") dep)) dep) (\k -> termNormal fill lv (p (Var nam dep)) dep)
  termNormalGo fill lv (Txt val)         dep = Txt val
  termNormalGo fill lv (Nat val)         dep = Nat val
  termNormalGo fill lv (Var nam idx)     dep = Var nam idx
@ -375,7 +375,7 @@ termSimilar (Op2 aOpr aFst aSnd) (Op2 bOpr bFst bSnd) dep = do
  eFst <- termEqual aFst bFst dep
  eSnd <- termEqual aSnd bSnd dep
  envPure (eFst && eSnd)
-termSimilar (Mat aNam aX aZ aS aP) (Mat bNam bX bZ bS bP) dep = do
+termSimilar (Swi aNam aX aZ aS aP) (Swi bNam bX bZ bS bP) dep = do
  eX <- termEqual aX bX dep
  eZ <- termEqual aZ bZ dep
  eS <- termEqual (aS (Var (stringConcat aNam "-1") dep)) (bS (Var (stringConcat bNam "-1") dep)) dep
@ -437,7 +437,7 @@ termIdenticalGo (Op2 aOpr aFst aSnd) (Op2 bOpr bFst bSnd) dep =
  envBind (termIdentical aFst bFst dep) $ \iFst ->
  envBind (termIdentical aSnd bSnd dep) $ \iSnd ->
  envPure (iFst && iSnd)
-termIdenticalGo (Mat aNam aX aZ aS aP) (Mat bNam bX bZ bS bP) dep =
+termIdenticalGo (Swi aNam aX aZ aS aP) (Swi bNam bX bZ bS bP) dep =
  envBind (termIdentical aX bX dep) $ \iX ->
  envBind (termIdentical aZ bZ dep) $ \iZ ->
  envBind (termIdentical (aS (Var (stringConcat aNam "-1") dep)) (bS (Var (stringConcat bNam "-1") dep)) dep) $ \iS ->
@ -517,7 +517,7 @@ termUnifyIsRec fill uid (Let nam val bod) dep = termUnifyIsRec fill uid val dep
 termUnifyIsRec fill uid (Use nam val bod) dep = termUnifyIsRec fill uid val dep || termUnifyIsRec fill uid (bod (Var nam dep)) (dep + 1)
 termUnifyIsRec fill uid (Hol nam ctx)     dep = False
 termUnifyIsRec fill uid (Op2 opr fst snd) dep = termUnifyIsRec fill uid fst dep || termUnifyIsRec fill uid snd dep
-termUnifyIsRec fill uid (Mat nam x z s p) dep = termUnifyIsRec fill uid x dep || termUnifyIsRec fill uid z dep || termUnifyIsRec fill uid (s (Var (stringConcat nam "-1") dep)) (dep + 1) || termUnifyIsRec fill uid (p (Var nam dep)) dep
+termUnifyIsRec fill uid (Swi nam x z s p) dep = termUnifyIsRec fill uid x dep || termUnifyIsRec fill uid z dep || termUnifyIsRec fill uid (s (Var (stringConcat nam "-1") dep)) (dep + 1) || termUnifyIsRec fill uid (p (Var nam dep)) dep
 termUnifyIsRec fill uid (Src src val)     dep = termUnifyIsRec fill uid val dep
 termUnifyIsRec fill uid (Met bUid bSpn)   dep = case termReduceMet fill 2 bUid bSpn of
  (Met bUid bSpn) -> uid == bUid
@ -542,7 +542,7 @@ termUnifySubst lvl neo Set               = Set
 termUnifySubst lvl neo U60               = U60
 termUnifySubst lvl neo (Num n)           = Num n
 termUnifySubst lvl neo (Op2 opr fst snd) = Op2 opr (termUnifySubst lvl neo fst) (termUnifySubst lvl neo snd)
-termUnifySubst lvl neo (Mat nam x z s p) = Mat nam (termUnifySubst lvl neo x) (termUnifySubst lvl neo z) (\k -> termUnifySubst lvl neo (s k)) (\k -> termUnifySubst lvl neo (p k))
+termUnifySubst lvl neo (Swi nam x z s p) = Swi nam (termUnifySubst lvl neo x) (termUnifySubst lvl neo z) (\k -> termUnifySubst lvl neo (s k)) (\k -> termUnifySubst lvl neo (p k))
 termUnifySubst lvl neo (Txt txt)         = Txt txt
 termUnifySubst lvl neo (Nat val)         = Nat val
 termUnifySubst lvl neo (Var nam idx)     = if lvl == idx then neo else Var nam idx
@ -613,7 +613,7 @@ termInferGo (Op2 opr fst snd) dep = do
  envSusp (Check 0 fst U60 dep)
  envSusp (Check 0 snd U60 dep)
  return U60
-termInferGo (Mat nam x z s p) dep = do
+termInferGo (Swi nam x z s p) dep = do
  envSusp (Check 0 x U60 dep)
  envSusp (Check 0 (p (Ann False (Var nam dep) U60)) Set dep)
  envSusp (Check 0 z (p (Num 0)) dep)
@ -753,19 +753,19 @@ termShow Set dep = "*"
 termShow U60 dep = "#U60"
 termShow (Num val) dep =
  let val' = u60Show val
-  in stringJoin ["#" , val']
+  in stringJoin [val']
 termShow (Op2 opr fst snd) dep =
  let opr' = operShow opr
      fst' = termShow fst dep
      snd' = termShow snd dep
-  in stringJoin ["#(" , opr' , " " , fst' , " " , snd' , ")"]
-termShow (Mat nam x z s p) dep =
+  in stringJoin ["(" , opr' , " " , fst' , " " , snd' , ")"]
+termShow (Swi nam x z s p) dep =
  let nam' = nam
      x'   = termShow x dep
      z'   = termShow z dep
      s'   = termShow (s (Var (stringConcat nam "-1") dep)) (dep + 1)
      p'   = termShow (p (Var nam dep)) dep
-  in stringJoin ["#match " , nam' , " = " , x' , " { #0: " , z' , " #+: " , s' , " }: " , p']
+  in stringJoin ["switch " , nam' , " = " , x' , " { #0: " , z' , " #+: " , s' , " }: " , p']
 termShow (Txt txt) dep = stringJoin [quote , txt , quote]
 termShow (Nat val) dep = show val
 termShow (Hol nam ctx) dep = stringJoin ["?" , nam]
--- a/src/term/compile.rs
+++ b/src/term/compile.rs
@ -37,88 +37,6 @@ impl Term {

  pub fn to_hvm1(&self, _env: im::Vector<String>, _met: &mut usize) -> String {
    todo!()
-    //fn binder(name: &str) -> String {
-      //format!("x{}", name.replace("-", "._."))
-    //}
-    //match self {
-      //Term::All { nam, inp, bod } => {
-        //let inp = inp.to_hvm1(env.clone(), met);
-        //let bod = bod.to_hvm1(cons(&env, nam.clone()), met);
-        //format!("(All \"{}\" {} λ{} {})", nam, inp, binder(nam), bod)
-      //},
-      //Term::Lam { nam, bod } => {
-        //let bod = bod.to_hvm1(cons(&env, nam.clone()), met);
-        //format!("(Lam \"{}\" λ{} {})", nam, binder(nam), bod)
-      //},
-      //Term::App { fun, arg } => {
-        //let fun = fun.to_hvm1(env.clone(), met);
-        //let arg = arg.to_hvm1(env.clone(), met);
-        //format!("(App {} {})", fun, arg)
-      //},
-      //Term::Ann { val, typ } => {
-        //let val = val.to_hvm1(env.clone(), met);
-        //let typ = typ.to_hvm1(env.clone(), met);
-        //format!("(Ann {} {})", val, typ)
-      //},
-      //Term::Slf { nam, typ, bod } => {
-        //let typ = typ.to_hvm1(env.clone(), met);
-        //let bod = bod.to_hvm1(cons(&env, nam.clone()), met);
-        //format!("(Slf \"{}\" {} λ{} {})", nam, typ, binder(nam), bod)
-      //},
-      //Term::Ins { val } => {
-        //let val = val.to_hvm1(env.clone(), met);
-        //format!("(Ins {})", val)
-      //},
-      //Term::Set => {
-        //"(Set)".to_string()
-      //},
-      //Term::U60 => {
-        //"(U60)".to_string()
-      //},
-      //Term::Num { val } => {
-        //format!("(Num {})", val)
-      //},
-      //Term::Op2 { opr, fst, snd } => {
-        //let fst = fst.to_hvm1(env.clone(), met);
-        //let snd = snd.to_hvm1(env.clone(), met);
-        //format!("(Op2 {} {} {})", opr.to_hvm1(), fst, snd)
-      //},
-      //Term::Mat { nam, x, z, s, p } => {
-        //let x = x.to_hvm1(env.clone(), met);
-        //let z = z.to_hvm1(env.clone(), met);
-        //let s = s.to_hvm1(cons(&env, format!("{}-1", nam)), met);
-        //let p = p.to_hvm1(cons(&env, nam.clone()), met);
-        //format!("(Mat \"{}\" {} {} λ{} {} λ{} {})", nam, x, z, binder(&format!("{}-1", nam)), s, binder(nam), p)
-      //},
-      //Term::Txt { txt } => {
-        //format!("(Txt \"{}\")", txt)
-      //},
-      //Term::Let { nam, val, bod } => {
-        //let val = val.to_hvm1(env.clone(), met);
-        //let bod = bod.to_hvm1(cons(&env, nam.clone()), met);
-        //format!("(Let \"{}\" {} λ{} {})", nam, val, binder(nam), bod)
-      //},
-      //Term::Hol { nam } => {
-        //let env_str = env.iter().map(|n| binder(n)).collect::<Vec<_>>().join(",");
-        //format!("(Hol \"{}\" [{}])", nam, env_str)
-      //},
-      //Term::Met {} => { 
-        //let n = *met; 
-        //*met += 1; 
-        //format!("(Met {})", n) 
-      //},
-      //Term::Var { nam } => {
-        //if env.contains(nam) { 
-          //format!("{}", binder(nam)) 
-        //} else { 
-          //format!("(Book.{})", nam) 
-        //}
-      //},
-      //Term::Src { src, val } => {
-        //let val = val.to_hvm1(env, met);
-        //format!("(Src {} {})", src.to_u64(), val)
-      //},
-    //}
  }
  
  pub fn to_hs_name(name: &str) -> String {
@ -169,12 +87,12 @@ impl Term {
        let snd = snd.to_hs(env.clone(), met);
        format!("(Op2 {} {} {})", opr.to_hs(), fst, snd)
      },
-      Term::Mat { nam, x, z, s, p } => {
+      Term::Swi { nam, x, z, s, p } => {
        let x = x.to_hs(env.clone(), met);
        let z = z.to_hs(env.clone(), met);
        let s = s.to_hs(cons(&env, format!("{}-1", nam)), met);
        let p = p.to_hs(cons(&env, nam.clone()), met);
-        format!("(Mat \"{}\" {} {} (\\{} -> {}) (\\{} -> {}))", nam, x, z, Term::to_hs_name(&format!("{}-1", nam)), s, Term::to_hs_name(nam), p)
+        format!("(Swi \"{}\" {} {} (\\{} -> {}) (\\{} -> {}))", nam, x, z, Term::to_hs_name(&format!("{}-1", nam)), s, Term::to_hs_name(nam), p)
      },
      Term::Let { nam, val, bod } => {
        let val = val.to_hs(env.clone(), met);
--- a/src/term/mod.rs
+++ b/src/term/mod.rs
@ -28,10 +28,10 @@ pub struct Src {
 //   SLF | $(<name>: <term>) <term>
 //   INS | ~<term>
 //   SET | *
-//   U60 | #U60
-//   NUM | #<uint>
-//   OP2 | #(<oper> <term> <term>)
-//   MAT | #match <name> = <term> { #0: <term>; #+: <term> }: <term>
+//   U60 | U60
+//   NUM | <uint>
+//   OP2 | (<oper> <term> <term>)
+//   SWI | switch <name> = <term> { 0: <term>; +: <term> }: <term>
 //   HOL | ?<name>
 //   MET | _
 //   CHR | '<char>'
@ -50,7 +50,7 @@ pub enum Term {
  U60,
  Num { val: u64 },
  Op2 { opr: Oper, fst: Box<Term>, snd: Box<Term> },
-  Mat { nam: String, x: Box<Term>, z: Box<Term>, s: Box<Term>, p: Box<Term> },
+  Swi { nam: String, x: Box<Term>, z: Box<Term>, s: Box<Term>, p: Box<Term> },
  Let { nam: String, val: Box<Term>, bod: Box<Term> },
  Use { nam: String, val: Box<Term>, bod: Box<Term> },
  Var { nam: String },
@ -131,7 +131,7 @@ impl Term {
        fst.get_free_vars(env.clone(), free_vars);
        snd.get_free_vars(env.clone(), free_vars);
      },
-      Term::Mat { nam, x, z, s, p } => {
+      Term::Swi { nam, x, z, s, p } => {
        x.get_free_vars(env.clone(), free_vars);
        z.get_free_vars(env.clone(), free_vars);
        s.get_free_vars(cons(&env, format!("{}-1",nam)), free_vars);
@ -198,7 +198,7 @@ impl Term {
        fst.desugar();
        snd.desugar();
      },
-      Term::Mat { nam: _, x, z, s, p } => {
+      Term::Swi { nam: _, x, z, s, p } => {
        x.desugar();
        z.desugar();
        s.desugar(); 
@ -284,8 +284,8 @@ impl Term {
          snd: Box::new(snd.clean()),
        }
      },
-      Term::Mat { nam, x, z, s, p } => {
-        Term::Mat {
+      Term::Swi { nam, x, z, s, p } => {
+        Term::Swi {
          nam: nam.clone(),
          x: Box::new(x.clean()),
          z: Box::new(z.clean()),
--- a/src/term/parse.rs
+++ b/src/term/parse.rs
@ -4,33 +4,71 @@ impl<'i> KindParser<'i> {

  pub fn parse_oper(&mut self) -> Result<Oper, String> {
    self.skip_trivia();
-    match self.peek_one() {
-      Some('+') => { self.advance_one(); Ok(Oper::Add) }
-      Some('-') => { self.advance_one(); Ok(Oper::Sub) }
-      Some('*') => { self.advance_one(); Ok(Oper::Mul) }
-      Some('/') => { self.advance_one(); Ok(Oper::Div) }
-      Some('%') => { self.advance_one(); Ok(Oper::Mod) }
-      Some('=') => { self.consume("==")?; Ok(Oper::Eq) }
-      Some('!') => { self.consume("!=")?; Ok(Oper::Ne) }
-      Some('<') => {
-        match self.peek_many(2) {
-          Some("<=") => { self.advance_many(2); Ok(Oper::Lte) }
-          Some("<<") => { self.advance_many(2); Ok(Oper::Lsh) }
-          _ => { self.advance_one(); Ok(Oper::Lt) }
-        }
-      }
-      Some('>') => {
-        match self.peek_many(2) {
-          Some(">=") => { self.advance_many(2); Ok(Oper::Gte) }
-          Some(">>") => { self.advance_many(2); Ok(Oper::Rsh) }
-          _ => { self.advance_one(); Ok(Oper::Gt) }
-        }
-      }
-      Some('&') => { self.advance_one(); Ok(Oper::And) }
-      Some('|') => { self.advance_one(); Ok(Oper::Or) }
-      Some('^') => { self.advance_one(); Ok(Oper::Xor) }
-      _ => self.expected("operator"),
+    if self.peek_one() == Some('+') {
+      self.consume("+")?;
+      return Ok(Oper::Add);
    }
+    if self.peek_one() == Some('-') {
+      self.consume("-")?;
+      return Ok(Oper::Sub);
+    }
+    if self.peek_one() == Some('*') {
+      self.consume("*")?;
+      return Ok(Oper::Mul);
+    } 
+    if self.peek_one() == Some('/') {
+      self.consume("/")?;
+      return Ok(Oper::Div);
+    }
+    if self.peek_one() == Some('%') {
+      self.consume("%")?;
+      return Ok(Oper::Mod);
+    }
+    if self.peek_many(2) == Some("==") {
+      self.consume("==")?;
+      return Ok(Oper::Eq);
+    }
+    if self.peek_many(2) == Some("!=") {
+      self.consume("!=")?;
+      return Ok(Oper::Ne); 
+    }
+    if self.peek_many(2) == Some("<=") {
+      self.consume("<=")?;
+      return Ok(Oper::Lte);
+    }
+    if self.peek_many(2) == Some("<<") {
+      self.consume("<<")?;
+      return Ok(Oper::Lsh);
+    }
+    if self.peek_one() == Some('<') { 
+      self.consume("<")?;
+      return Ok(Oper::Lt);
+    }
+    if self.peek_many(2) == Some(">=") {
+      self.consume(">=")?;
+      return Ok(Oper::Gte); 
+    }
+    if self.peek_many(2) == Some(">>") {
+      self.consume(">>")?;
+      return Ok(Oper::Rsh);
+    }
+    if self.peek_one() == Some('>') {
+      self.consume(">")?;
+      return Ok(Oper::Gt);
+    }
+    if self.peek_one() == Some('&') {
+      self.consume("&")?;
+      return Ok(Oper::And);
+    }
+    if self.peek_one() == Some('|') {
+      self.consume("|")?;
+      return Ok(Oper::Or);
+    } 
+    if self.peek_one() == Some('^') {
+      self.consume("^")?;
+      return Ok(Oper::Xor);
+    }
+    self.expected("operator")
  }

  pub fn parse_term(&mut self, fid: u64, uses: &Uses) -> Result<Term, String> {
@ -65,7 +103,6 @@ impl<'i> KindParser<'i> {

    // RFL ::= (=)
    if self.starts_with("{=}") {
-      // returns the same as if we parsed the "(Equal.refl _ _)" application
      let ini = *self.index() as u64;
      self.consume("{=}")?;
      let end = *self.index() as u64;
@ -82,10 +119,24 @@ impl<'i> KindParser<'i> {
      });
    }

-    // APP ::= (<term> <term>)
+    // OP2 ::= (<oper> <term> <term>)
+    // APP ::= (<term> <term> ...)
    if self.starts_with("(") {
      let ini = *self.index() as u64;
      self.consume("(")?;
+      // Operation
+      if let Some(oper) = self.peek_one() {
+        if "+-*/%=&|<>!^".contains(oper) {
+          let opr = self.parse_oper()?;
+          let fst = Box::new(self.parse_term(fid, uses)?);
+          let snd = Box::new(self.parse_term(fid, uses)?);
+          self.consume(")")?;
+          let end = *self.index() as u64;
+          let src = Src::new(fid, ini, end);
+          return Ok(Term::Src { src, val: Box::new(Term::Op2 { opr, fst, snd }) });
+        }
+      }
+      // Application
      let fun = Box::new(self.parse_term(fid, uses)?);
      let mut args = Vec::new();
      while self.peek_one() != Some(')') {
@ -164,34 +215,12 @@ impl<'i> KindParser<'i> {
      return Ok(Term::Src { src, val: Box::new(Term::Set) });
    }

-    // U60 ::= #U60
-    if self.starts_with("#U60") {
-      let ini = *self.index() as u64;
-      self.consume("#U60")?;
-      let end = *self.index() as u64;
-      let src = Src::new(fid, ini, end);
-      return Ok(Term::Src { src, val: Box::new(Term::U60) });
-    }
-
-    // OP2 ::= #(<oper> <term> <term>)
-    if self.starts_with("#(") {
-      let ini = *self.index() as u64;
-      self.consume("#(")?;
-      let opr = self.parse_oper()?;
-      let fst = Box::new(self.parse_term(fid, uses)?);
-      let snd = Box::new(self.parse_term(fid, uses)?);
-      self.consume(")")?;
-      let end = *self.index() as u64;
-      let src = Src::new(fid, ini, end);
-      return Ok(Term::Src { src, val: Box::new(Term::Op2 { opr, fst, snd }) });
-    }
-
-    // MAT ::= #match <name> = <term> { #0: <term>; #+: <term> }: <term>
+    // SWI ::= switch <name> = <term> { 0: <term>; +: <term> }: <term>
    // - The matched term is optional. Defaults to `Var { nam: <name> }`.
    // - The return type is optional. Defaults to `Met {}`.
-    if self.starts_with("#match") {
+    if self.starts_with("switch ") {
      let ini = *self.index() as u64;
-      self.consume("#match")?;
+      self.consume("switch ")?;
      let nam = self.parse_name()?;
      self.skip_trivia();
      let x = if self.peek_one() == Some('=') {
@ -201,11 +230,9 @@ impl<'i> KindParser<'i> {
        Box::new(Term::Var { nam: nam.clone() })
      };
      self.consume("{")?;
-      self.consume("#0")?;
-      self.consume(":")?;
+      self.consume("0:")?;
      let z = Box::new(self.parse_term(fid, uses)?);
-      self.consume("#+")?;
-      self.consume(":")?;
+      self.consume("+:")?;
      let s = Box::new(self.parse_term(fid, &shadow(&format!("{}-1",nam), uses))?);
      self.consume("}")?;
      let p = if self.peek_one() == Some(':') {
@ -216,17 +243,18 @@ impl<'i> KindParser<'i> {
      };
      let end = *self.index() as u64;
      let src = Src::new(fid, ini, end);
-      return Ok(Term::Src { src, val: Box::new(Term::Mat { nam, x, z, s, p }) });
+      return Ok(Term::Src { src, val: Box::new(Term::Swi { nam, x, z, s, p }) });
    }

-    // NUM ::= #<uint>
+    // NAT ::= #<uint>
    if self.starts_with("#") {
      let ini = *self.index() as u64;
      self.advance_one();
      let val = self.parse_u64()?;
      let end = *self.index() as u64;
      let src = Src::new(fid, ini, end);
-      return Ok(Term::Src { src, val: Box::new(Term::Num { val }) });
+      let val = Box::new(Term::new_nat(val));
+      return Ok(Term::Src { src, val });
    }

    // HOL ::= ?<name>
@ -302,13 +330,13 @@ impl<'i> KindParser<'i> {
      return Ok(Term::Src { src, val });
    }

-    // NAT ::= <uint>
+    // NUM ::= <uint>
    if self.peek_one().map_or(false, |c| c.is_ascii_digit()) {
      let ini = *self.index() as u64;
-      let nat = self.parse_u64()?;
+      let val = self.parse_u64()?;
      let end = *self.index() as u64;
      let src = Src::new(fid, ini, end);
-      let val = Box::new(Term::new_nat(nat));
+      let val = Box::new(Term::Num { val });
      return Ok(Term::Src { src, val });
    }

@ -323,31 +351,28 @@ impl<'i> KindParser<'i> {
      return Ok(Term::Src { src, val: Box::new(Term::new_adt(&adt)) });
    }

-    // MAT ::= match <name> = <term> { <name> : <term> <...> }: <term>
+    // MCH ::= match <name> = <term> { <name> : <term> <...> }: <term>
    if self.starts_with("match ") {
      let ini = *self.index() as u64;
      let mch = self.parse_match(fid, uses)?;
      let end = *self.index() as u64;
      let src = Src::new(fid, ini, end);
      return Ok(Term::Src { src, val: Box::new(Term::Mch { mch: Box::new(mch) }) });
-      //return Ok(Term::Src { src, val: Box::new(Term::new_match(&mch)) });
    }

    // VAR ::= <name>
    let ini = *self.index() as u64;
    let old = self.parse_name()?;
    let nam = uses.get(&old).unwrap_or(&old).to_string();
-    //if old != nam { println!("{} -> {}", old, nam); }
    let end = *self.index() as u64;
    let src = Src::new(fid, ini, end);
-    return Ok(Term::Src { src, val: Box::new(Term::Var { nam }) });
+    let val = if nam == "U60" {
+      Box::new(Term::U60)
+    } else {
+      Box::new(Term::Var { nam })
+    };
+    return Ok(Term::Src { src, val });

  }

-  // Parses a name that can be aliased (via the 'uses' map)
-  //pub fn parse_nick(&mut self, uses: &Uses) -> Result<String, String> {
-    //let nam = self.parse_name()?;
-    //Ok(uses.get(&nam).cloned().unwrap_or(nam))
-  //}
-
 }
--- a/src/term/show.rs
+++ b/src/term/show.rs
@ -169,21 +169,21 @@ impl Term {
          Show::text(")"),
        ])
      },
-      Term::Mat { nam, x, z, s, p } => {
+      Term::Swi { nam, x, z, s, p } => {
        Show::call(" ", vec![
          Show::glue(" ", vec![
-            Show::text("#match"),
+            Show::text("switch"),
            Show::text(nam),
            Show::text("="),
            x.format_go(),
            Show::text("{"),
          ]),
          Show::glue("", vec![
-            Show::text("#0: "),
+            Show::text("0: "),
            z.format_go(),
          ]),
          Show::glue("", vec![
-            Show::text("#+: "),
+            Show::text("+: "),
            s.format_go(),
            Show::text(" "),
          ]),