Skip to content

Latest commit

 

History

History
4 lines (3 loc) · 219 Bytes

readme.md

File metadata and controls

4 lines (3 loc) · 219 Bytes

Lambda2

This is a very hastily-written notation-less implementation of lambda2 system in Coq.
For more information, see chapter three of Type Theory and Formal Proof, an Introduction, by Nederpelt and Geuvers.