Lambda Documentation

Add lambda documentation specifying the indexing of free variables.

src/lambda/lambda.lisp

@@ -77,13 +77,13 @@ per above description. While not always, not doing so result in an error upon
 evaluation. As an example of a valid entry we have
 
 ```lisp
- (ann-term1 (list so1 (fun-type so1 so1)) (app (index 1) (index 0)))
+ (ann-term1 (list so1 (fun-type so1 so1)) (app (index 1) (list (index 0))))
 ```
 
 while
 
 ```lisp
-(ann-term1 (list so1 (so-hom-obj so1 so1)) (app (index 1) (index 0)))
+(ann-term1 (list so1 (so-hom-obj so1 so1)) (app (index 1) (list (index 0))))
 ```
 
 produces an error trying to use [HOM-COD]. This warning applies to other

src/specs/lambda.lisp

@@ -363,7 +363,18 @@ or equivalently
 (so-hom-obj so1 (so-hom-obj so0 so0))
 ```
 
-due to Geb's computational definition of the function type."))
+due to Geb's computational definition of the function type.
+
+Note that [INDEX][class] 0 in the above code is of type [SO1][class]
+so the counting of indeces starts with the leftmost argument for
+computational reasons. In practice, typing of [LAMB][class] corresponds with
+taking a list of arguments provided to a lambda term, making it a context
+in that order and then counting the index of the varibale. Type-theoretically,
+
+$$\vdash \\lambda \\Gamma (index i)$$
+$$\\Gamma \\vdash (index i)$$
+
+For further info, consult [INDEX][class]."))
 
 (defun lamb (tdom term &key (ttype nil))
   (make-instance 'lamb :tdom tdom :term term :ttype ttype))