Solutions

Lexical version of DefineDatatype

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 website here.
 Roshan: Uploaded an interpreter for the pure lambda calculus. This interpreter uses lexical addressing for variables.

Same Fringe