Single Module Lambda Calculus from Simply Typed to Martin Lof Type Theory
1 points by solomon
1 points by solomon
This project had been on pause for a while but I recently got back into it. My end goal is a series of examples for implementing Bidrectional Typechecking and NbE for a variety of type system features.