Reservoir

remimimimimi/lambda-calculus-typecheckers

Implementation of different type theories in Lean4

GitHub Link Documentation

Pick a version!

TODO: should show a time axes that allows the users to view, filter and click copy the lakefile config.

README

Lean4 type theory

Implementation of different type theories in Lean4.

Build and run

Install elan, nightly version of Lean4. Choose directory and run lake build.