diff --git a/README.md b/README.md
index 3aac1d0d0..6e43c1d14 100644
--- a/README.md
+++ b/README.md
@@ -130,6 +130,56 @@ data List = (List.cons head tail) | (List.nil)
 ListEx2 = (List.cons 1 (List.cons 2 (List.cons 3 List.nil)))
 ```
 
+It's possible to match different kinds of terms. These three forms are equivalent:
+```rs
+match list {
+  (List.cons hd tl):  (Some hd)
+  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
+}
+
+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 (+ 0 1)) 5) {
+    0: "five"
+    _:  ...
+  }
+}
+```
+
+Match multiple terms:
+```rs
+λa λb match a, b {
+  (Some True) (x, y): (Some (x, y))
+  (Some False) (x, y): (Some (y, x))
+  None *: None
+}
+```
+
 ### More features
 
 Key:
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..460d7c91f 100644
--- a/docs/native-numbers.md
+++ b/docs/native-numbers.md
@@ -34,22 +34,22 @@ 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
-    +: (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 
+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 
+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,12 @@ 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, 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))
   }
 
 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.