[lambda-calculus.wtn] add note about de brujin indexing

format.c

@@ -288,7 +288,7 @@ main(int argc, char *argv[])
         char bn[80] = {0};
         basename(argv[1], bn, '.');
 
-        char out_name[80] = {0};
+        char out_name[85] = {0};
         sprintf(out_name, "%s.html", bn);
 
         out = fopen(out_name, "w");

site-src/lambda-calculus.wtn

@@ -21,6 +21,11 @@ expression following the period. λx.x is therefore the function that takes one
 argument and evaluates to that argument. An example of applying this function is
 (λx.x) y → y.
 
+Using De Brujin indexing, variable names are no longer necessary. With this
+indexing system, each variable name instance is replaced by an index. The
+K-combinator (λx.λy.x) is expressed with De Brujin indexing as λ λ 2. The '2' is
+the index, which refers to the variable bound by the lambda form 2 levels.
+
 ** Reduction
 
 There are two ways of reducing an expression, α-conversion and