Recursion improvements

docs/source/tutorials/Boxes.md

@@ -109,29 +109,3 @@ main : !Word
 
 We "emulate" a recursive function by using `ten_times` to "build" the recursion tree of "fact" up to 10 layers deep. As such, it only works for inputs up to 10; after that, it hits the "halt" case and returns 0. The good thing about this way of doing recursion is that we're not limited to recurse on structurally smaller arguments. The bad thing is that it is a little bit verbose, requiring an explicit bound, and a halting case for when the function "runs out of gas". Moreover, since we used `ten_times` to make the function, it comes inside a box, on `level 1`. In other words, it is impossible to use it on `level 0`! Instead, we must use the `level 0` to unbox it (with a `dup`), and then use it on `level 1`.
 
-Fortunately, since bounded recursive functions are so common, Formality has built-in syntax for them, relying on "boxed definitions". To make a boxed definition, simply annotate it with a `!` instead of a `:`. That has several effects. First, the whole definition is lifted to `level 1`. Second, it allows you to use boxed definitions inside `<>`s: the parser will automatically unbox them for you. Third, the definition can call itself recursively; if it does, then Formality will assembling the recursion for you using a `Ind` implementation from the Base library. This is an example of usage:
-
-```javascript
-!fact*n : ! {i : Word} -> Word
-  cpy i = i
-  if i .= 0:
-    1
-  else:
-    i * fact(i - 1)
-  * 0
-
-!main : !Word
-  <fact*100>(12)
-```
-
-Notice that the halting case was defined with a `*` on the end. If it coincided with one of the function's arguments, you could place a `*` before it instead, i.e., `fact ! {*i : Word} -> Word`. Note also that, since `main` uses a recursive function, it must itself be a boxed definition, annotated with `!`. Alternatively, you could make it a normal definition and perform the unboxing yourself:
-
-```javascript
-main : !Word
-  dup fact = fact*100
-  # fact(12)
-```
-
-Both are equivalent.
-
-The maximum recursion depth of the `Ind` defined by the base library is `2^256-1`. In other words, despite being terminating, in practice, Formality is capable of doing anything a Turing-complete language could do. After all, no language could perform more than `2^256-1` calls without exhausting your computer (or this universe's) resources.

docs/source/tutorials/Recursion.md

@@ -1,6 +1,58 @@
 # Recursion
 
-(TODO)
+## Boxed definitions
+
+Since bounded recursive functions are so common, Formality has built-in syntax for them, relying on "boxed definitions". To make a boxed definition, simply annotate it with a `!` instead of a `:`. That has two effects. First, the whole definition is lifted to `level 1`. Second, it allows you to use boxed definitions inside `<>`s: the parser will automatically unbox them for you. For example, instead of this:
+
+```javascript
+foo : !Word
+  #40
+
+bar : !Word
+  #2
+
+main : !Word
+  dup foo = foo
+  dup bar = bar
+  # foo + bar
+```
+
+We could write:
+
+```javascript
+!foo : !Word
+  40
+
+!bar : !Word
+  2
+
+!main : !Word
+  <foo> + <bar>
+```
+
+Both programs are the same, except the later is shorter.
+
+## Recursion
+
+Formality allows you to turn a boxed definition into a recursive function by appending `*N` to its name (where `N` is a new variable, which will track how many times the function was called), and adding a "halt-case" with a `* term` on the last line (where `term` is an expression that will be returned if the function hits its call limit). So, for example, a factorial function could be written as:
+
+```javascript
+!fact*n : ! {i : Word} -> Word
+  if i .= 0:
+    1
+  else:
+    i * fact(i - 1)
+  * 0
+
+!main : !Word
+  <fact*100>(12)
+```
+
+This is not much different from the usual `fact` definition, except we explicitly set the "halt-case" to be `0` on the last line. That means that, if the function "runs out of gas", it will stop and return `0` instead. As a shortcut, if your "halt-case" is simply one of the function's argument, you can write the `*` on it instead, as in, `fact ! {*i : Word} -> Word`. 
+
+The maximum recursion depth of the `Ind` defined by the base library is `2^256-1`. In other words, despite being terminating, in practice, Formality is capable of doing anything a Turing-complete language could do. After all, no language could perform more than `2^256-1` calls without getting a stack-overflow, or exhausting your computer's CPU/memory.
+
+## (TODO)
 
 Cover things like:
 
@@ -18,7 +70,7 @@ Cover things like:
 - Polymorphic recursive functions with level-0 parameters
 
     ```javascript
-    !map*n : {~A : Type, ~B : Type, f : !A -> B} -> ! {case list : List(A)} -> List(B)
+    !map*N : {~A : Type, ~B : Type, f : !A -> B} -> ! {case list : List(A)} -> List(B)
     | cons => cons(~B, f(list.head), map(list.tail))
     | nil  => nil(~B)
     * nil(~B)
@@ -27,7 +79,14 @@ Cover things like:
       <map*(~Word, ~Word, #{x} x + 1)>(Word$[1,2,3,4])
     ```
 
-- Advanced, Agda-like structural recursion with Bounds
+- Indexed recursive functions using `N`
+
+```javascript
+... vector stuff, fin stuff, etc...
+```
+
+
+- Structural recursive proofs with Bounds
 
 ```javascript
 // ∀ n . n < n+1
@@ -43,4 +102,5 @@ Cover things like:
   * absurd(absurd_bound(n, bound), ~Less(n, succ(n)))
 ```
 
+
 etc.