This project will eventually be a reference type-checker for the Lean theorem prover: a simple and small program that can type-check fully elaborated Lean terms, exported in the following low-level format:
https://github.com/leanprover/lean/blob/master/doc/export_format.md
The main Lean repository can be found at:
https://github.com/leanprover/lean
The code follows the design of the Lean kernel closely, except can be made simpler since it does not need to integrate with parsing and elaboration, and because it need not be as performant.
This project uses the new Stack Haskell build system. More information can be found at: