Add more details to documentation.

Add documentation for bitwise NOT, extra details on how scopeless lambdas and lazy definitions work.

docs/lazy-definitions.md

@@ -1,9 +1,43 @@
 # Making recursive definitions lazy
 
-The HVM-Core is an eager runtime, for both CPU and parallel GPU implementations. Recursive terms will unroll indefinitely.
+The HVM-Core is an eager runtime, for both CPU and parallel GPU implementations. Terms that use ecursive terms will unroll indefinitely.
+
+This means that for example, the following code will hang, despite being technically correct and working on Haskell:
+
+```rs
+data Nat = Z | (S p)
+
+Y = λf (λx (f (x x)) λx (f (x x)))
+
+Nat.add = (Y λaddλaλb match a {
+	Z: b
+	(S p): (S (add p b))
+})
+
+main = (Nat.add (S (S (S Z))) (S Z))
+```
 
 Because of that, is recommended to use [supercombinator](https://en.wikipedia.org/wiki/Supercombinator) formulation to make terms be unrolled lazily, preventing infinite expansion in recursive function bodies.
 
+Supercombinators are simply closed terms. Supercombinator formulation is writing the program as a composition of supercombinators. In this case, `Nat.add` can be a supercombinator.
+
+```rs
+data Nat = Z | (S p)
+
+Nat.add = λaλb match a {
+	Z: b
+	(S p): (S (Nat.add p b))
+}
+
+main = (Nat.add (S (S (S Z))) (S Z))
+```
+
+This code will work as expected, because `Nat.add` is unrolled lazily only when it is used as an argument to a lambda.
+
+### Automatic optimization
+
+HVM-lang carries out an optimization automatically:
+
 Consider the code below:
 ```rs
 Zero = λf λx x
@@ -16,5 +50,3 @@ ToMachine0 = λp (+ 1 (ToMachine p))
 ToMachine = λn (n ToMachine0 0)
 ```
 Definitions are lazy in the runtime. Lifting lambda terms to new definitions will prevent infinite expansion.
-
-This optimization is done automatically by hvm-lang.

docs/native-numbers.md

@@ -23,6 +23,15 @@ some_val = (+ (+ 7 4) (* 2 3))
 ```
 The current operations include `+, -, *, /, %, ==, !=, <, >, <=, >=, &, |, ^, ~, <<, >>`.
 
+The `~` symbol stands for NOT. It takes two arguments and calculates the 60-bit binary NOT of the first one, but ignores its second one. However, because of implementation details, the second argument must be a number too.
+
+```rs
+main = (~ 42 10)
+// Outputs the same thing as (~ 42 50)
+// And as (~ 42 1729)
+// But not the same thing as (~ 42 *) (!)
+```
+
 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 
@@ -45,7 +54,7 @@ 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 the predecessor to `a`
+    // If the number is greater than 0, bind it predecessor to `a`
     +a:
     match a {
       // If the predecessor is 0, then return 1

docs/using-scopeless-lambdas.md

@@ -12,11 +12,20 @@ Of course, using scopeless lambdas as a replacement for regular lambdas is kind
 
 ```rs
 main = (((λ$x 1) 2), $x)
-// ---- x gets replaced by 2 and application gets replaced by 1
+// $x gets replaced by 2 and the application ((λ$x 1) 2) gets replaced by 1
 // Outputs (1, 2)
 ```
 
-Take some time to think about the program above. It is valid, despite `$x` being used outside the body.
+Take some time to think about the program above. It is valid, despite `$x` being used outside the lambda's body.
+
+However, scopeless lambdas don't bind across definitions
+```rs
+def = $x
+
+main = (((λ$x 1) 2), def)
+```
+
+The bound variables are local to each term.
 
 ## Duplicating scopeless lambdas
 
@@ -26,10 +35,8 @@ We have seen that the variable bound to a scopeless lambda gets set when the lam
 main = // TODO bug in hvm-lang
 	let _ = λ$x 1 // Discard and erase the scopeless lambda
 	(2, $x)
-```
-Output:
-```rs
-(2, *)
+
+// Outputs (2, *)
 ```
 
 The program outputs `2` as the first item of the tuple, as expected. But the second item is `*`! What is `*`?
@@ -44,10 +51,8 @@ Try to answer this with your knowledge of HVM. Will it throw a runtime error? Wi
 main =
 	let f = λ$x 1 // Assign the lambda to a variable
 	((f 2), ((f 3), $x)) // Return a tuple of (f 2) and another tuple.
-```
-Output:
-```
-(1, (1, {#0 3 2}))
+
+// Outputs (1, (1, {#0 3 2}))
 ```
 
 What? This is even more confusing. The first two values are `1`, as expected. But what about the last term?

examples/callcc.hvm

@@ -1,3 +1,5 @@
+// This program is an example that shows how scopeless lambdas can be used.
+
 Seq a b = a
 
 // Create a program capable of using `callcc`