Improve docs and update examples with new match syntax

README.md

@@ -130,7 +130,7 @@ data List = (List.cons head tail) | (List.nil)
 ListEx2 = (List.cons 1 (List.cons 2 (List.cons 3 List.nil)))
 ```
 
-Match different kinds of terms, both matches are equivalent:
+It's possible to match different kinds of terms. These three forms are equivalent:
 ```rs
 match list {
   (List.cons hd tl):  (Some hd)
@@ -162,7 +162,7 @@ Which is the equivalent of nesting match terms:
 ```rs
 match 4 {
   0: "zero"
-  1+a: match (- a 4) {
+  1+a: match (- (+ a (+ 0 1)) 5) {
     0: "five"
     _:  ...
   }
@@ -171,9 +171,10 @@ match 4 {
 
 Match multiple terms:
 ```rs
-match True, True {
-  True True:  True
-  _ _: False
+λa λb match a, b {
+  (Some True) (x, y): (Some (x, y))
+  (Some False) (x, y): (Some (y, x))
+  None *: None
 }
 ```
 

cspell.json

@@ -42,6 +42,7 @@
     "namegen",
     "nams",
     "numop",
+    "nums",
     "oper",
     "opre",
     "oprune",

docs/compiler-options.md

@@ -142,20 +142,20 @@ When the `linearize-matches` option is used, linearizes only vars that are used
 
 Example:
 ```rs
-λa λb match a { 0: b; +: b }
+λa λb match a { 0: b; 1+: b }
 
 // Is transformed to
-λa λb (match a { 0: λc c; +: λd d } b)
+λa λb (match a { 0: λc c; 1+: λd d } b)
 ```
 
 When the `linearize-matches-extra` option is used, linearizes all vars used in the arms.
 
 example:
 ```rs
-λa λb λc match a { 0: b; +: c }
+λa λb λc match a { 0: b; 1+: c }
 
 // Is transformed to
-λa λb λc (match a { 0: λd λ* d; +: λ* λe e } b c)
+λa λb λc (match a { 0: λd λ* d; 1+: λ* λe e } b c)
 ```
 
 ## float-combinators

docs/native-numbers.md

@@ -37,19 +37,19 @@ HVM-lang also includes a `match` syntax for native numbers. The `0` case is chos
 Number.to_church = λn λf λx 
   match n {
     0: x
-    +: (f (Number.to_church n-1 f x))
+    1+: (f (Number.to_church n-1 f x))
   }
 // Alternative syntax
 Number.to_church = λn λf λx 
   match n {
     0: x
-    +p: (f (Number.to_church p f x))
+    1+p: (f (Number.to_church p f x))
   }
 // Alternative syntax with name binding
 Number.to_church = λn λf λx 
   match num = n {
     0: x
-    +: (f (Number.to_church num-1 f x)
+    1+: (f (Number.to_church num-1 f x)
   }
 ```
 
@@ -60,14 +60,10 @@ fibonacci = λn // n is the argument
   match n {
     // If the number is 0, then return 0
     0: 0
-    // If the number is greater than 0, bind it predecessor to `a`
-    +a:
-    match a {
-      // If the predecessor is 0, then return 1
-      0: 1
-      // Otherwise, bind n-2 to `b` and return the sum of (fib n-1) and (fib n-2)
-      +b: (+ (fibonacci a) (fibonacci b))
-    }
+    // If the number is 1, then return 1
+    1: 1
+    // Otherwise, and return the sum of (fib (n-2 + 1)) and (fib n-2)
+    2+: (+ (fibonacci (+ n-2 1)) (fibonacci n-2))
   }
 
 main = (fibonacci 15)

docs/writing-fusing-functions.md

@@ -130,7 +130,7 @@ not = λboolean (boolean false true)
 fusing_not = λboolean λt λf (boolean f t)
 // Creates a Church numeral out of a native number
 to_church 0 = λf λx x
-to_church +p = λf λx (f (to_church p f x))
+to_church 1+p = λf λx (f (to_church p f x))
 main =
 	let two = λf λx (f (f x))
 	let two_pow_512 = ((to_church 512) two) // Composition of church-encoded numbers is equivalent to exponentiation.

examples/example.hvm

@@ -22,7 +22,7 @@
 (Num.pred) = λn 
   match n { 
     0: 0
-    +: n-1
+    1+: n-1
   }
 
 // Write new data types like this

examples/fusing_not.hvm

@@ -4,7 +4,7 @@ not = λboolean (boolean false true)
 fusing_not = λboolean λt λf (boolean f t)
 // Creates a Church numeral out of a native number
 to_church 0 = λf λx x
-to_church +p = λf λx (f (to_church p f x))
+to_church 1+p = λf λx (f (to_church p f x))
 main = 
 	let two = λf λx (f (f x))
 	let two_pow_512 = ((to_church 512) two) // Composition of church-encoded numbers is equivalent to exponentiation.