Lexical version of Define-Datatype
Irrationality of sqrt(2)
You can place your proofs in /l/www/classes/b621/proofs.
- Matt: I put some interesting things about the X combinator (with respect to its definition and also expressing it interms of itself).
- Kyle: I've uploaded some code for assorted assignments on a page on my web-site here.
- Roshan: Uploaded an interpreter for the pure lambda calculus. This interpreter uses lexical addressing for variables.