From 03c60912830d86c4a9a82f45fa9040d3599a3a5f Mon Sep 17 00:00:00 2001
From: imaqtkatt <eduarda.so@proton.me>
Date: Tue, 27 Feb 2024 17:04:36 -0300
Subject: [PATCH 1/5] Add brief documentation about match syntax

---
 README.md | 47 +++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 47 insertions(+)

diff --git a/README.md b/README.md
index 3aac1d0d0..5829ddc52 100644
--- a/README.md
+++ b/README.md
@@ -130,6 +130,53 @@ 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:
+```rs
+match list {
+  (List.cons hd tl):  (Some hd)
+  List.nil:  None
+}
+
+match list {
+  List.cons:  (Some list.head)
+  List.nil:  None
+}
+
+match bind = list {
+  List.cons:  (Some bind.head)
+  List.nil:  None
+}
+```
+
+Match native numbers:
+```rs
+match 4 {
+  0:  "zero"
+  5:  "five"
+  4:  "four"
+  _:  "other"
+}
+```
+
+Which is the equivalent of nesting match terms:
+```rs
+match 4 {
+  0: "zero"
+  1+a: match (- a 4) {
+    0: "five"
+    _:  ...
+  }
+}
+```
+
+Match multiple terms:
+```rs
+match True, True {
+  True True:  True
+  _ _: False
+}
+```
+
 ### More features
 
 Key:

From a0dbd04791cd91c125fc31c602145f709d1a03b7 Mon Sep 17 00:00:00 2001
From: imaqtkatt <eduarda.so@proton.me>
Date: Tue, 27 Feb 2024 17:47:20 -0300
Subject: [PATCH 2/5] Improve docs and update examples with new match syntax

---
 README.md                        | 11 ++++++-----
 cspell.json                      |  1 +
 docs/compiler-options.md         |  8 ++++----
 docs/native-numbers.md           | 18 +++++++-----------
 docs/writing-fusing-functions.md |  2 +-
 examples/example.hvm             |  2 +-
 examples/fusing_not.hvm          |  2 +-
 7 files changed, 21 insertions(+), 23 deletions(-)

diff --git a/README.md b/README.md
index 5829ddc52..cc8624154 100644
--- a/README.md
+++ b/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
 }
 ```
 
diff --git a/cspell.json b/cspell.json
index fca40f4d3..7bd1f52e8 100644
--- a/cspell.json
+++ b/cspell.json
@@ -42,6 +42,7 @@
     "namegen",
     "nams",
     "numop",
+    "nums",
     "oper",
     "opre",
     "oprune",
diff --git a/docs/compiler-options.md b/docs/compiler-options.md
index 7ae6f75f7..4aaeb2c22 100644
--- a/docs/compiler-options.md
+++ b/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
diff --git a/docs/native-numbers.md b/docs/native-numbers.md
index 5edf79caa..d464345c5 100644
--- a/docs/native-numbers.md
+++ b/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)
diff --git a/docs/writing-fusing-functions.md b/docs/writing-fusing-functions.md
index fbb640cd5..6128033e2 100644
--- a/docs/writing-fusing-functions.md
+++ b/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.
diff --git a/examples/example.hvm b/examples/example.hvm
index 5170f5a92..ca7fe5a40 100644
--- a/examples/example.hvm
+++ b/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
diff --git a/examples/fusing_not.hvm b/examples/fusing_not.hvm
index af1262d10..0de7599b2 100644
--- a/examples/fusing_not.hvm
+++ b/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.

From 1b570712a4dc2467149645d478cace2a93cd62ce Mon Sep 17 00:00:00 2001
From: imaqtkatt <eduarda.so@proton.me>
Date: Wed, 28 Feb 2024 08:53:46 -0300
Subject: [PATCH 3/5] Fix native-numbers fib comment

---
 docs/native-numbers.md | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/docs/native-numbers.md b/docs/native-numbers.md
index d464345c5..29ee32dd4 100644
--- a/docs/native-numbers.md
+++ b/docs/native-numbers.md
@@ -34,19 +34,19 @@ main = (~ 42 10)
 
 HVM-lang also includes a `match` syntax for native numbers. The `0` case is chosen when `n` is 0, and the `+` case is chosen when `n` is greater than 0. The previous number, by default, bound to `n-1`.
 ```rs
-Number.to_church = λn λf λx 
+Number.to_church = λn λf λx
   match n {
     0: x
     1+: (f (Number.to_church n-1 f x))
   }
 // Alternative syntax
-Number.to_church = λn λf λx 
+Number.to_church = λn λf λx
   match n {
     0: x
     1+p: (f (Number.to_church p f x))
   }
 // Alternative syntax with name binding
-Number.to_church = λn λf λx 
+Number.to_church = λn λf λx
   match num = n {
     0: x
     1+: (f (Number.to_church num-1 f x)
@@ -62,7 +62,7 @@ fibonacci = λn // n is the argument
     0: 0
     // If the number is 1, then return 1
     1: 1
-    // Otherwise, and return the sum of (fib (n-2 + 1)) and (fib n-2)
+    // Otherwise, return the sum of (fib (n-2 + 1)) and (fib n-2)
     2+: (+ (fibonacci (+ n-2 1)) (fibonacci n-2))
   }
 

From d646ab00527a8bf63f39d0e407275f302f06e44e Mon Sep 17 00:00:00 2001
From: imaqtkatt <eduarda.so@proton.me>
Date: Wed, 28 Feb 2024 09:08:20 -0300
Subject: [PATCH 4/5] Add field bindings comment

---
 README.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/README.md b/README.md
index cc8624154..6e43c1d14 100644
--- a/README.md
+++ b/README.md
@@ -137,6 +137,8 @@ match list {
   List.nil:  None
 }
 
+// If we don't provide field bindings, it will implicitly use
+// the fields of the declared data type
 match list {
   List.cons:  (Some list.head)
   List.nil:  None

From 978efa3b62c0290c53e766dd6e71e370eccf2762 Mon Sep 17 00:00:00 2001
From: imaqtkatt <eduarda.so@proton.me>
Date: Wed, 28 Feb 2024 10:14:36 -0300
Subject: [PATCH 5/5] Improve native numbers doc

---
 docs/native-numbers.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/docs/native-numbers.md b/docs/native-numbers.md
index 29ee32dd4..460d7c91f 100644
--- a/docs/native-numbers.md
+++ b/docs/native-numbers.md
@@ -63,6 +63,8 @@ fibonacci = λn // n is the argument
     // If the number is 1, then return 1
     1: 1
     // Otherwise, return the sum of (fib (n-2 + 1)) and (fib n-2)
+    // The successor pattern provides a `var`-`successor number` bind
+    // and it's also possible to define other bind name `2+x`
     2+: (+ (fibonacci (+ n-2 1)) (fibonacci n-2))
   }