koi
(Kalculus Of Inductive constructions)
An Approachable Implementation of a Compiler for the Calculus of Inductive Constructions.
Blog Posts
Here is a series of blog posts that I wrote about this project.
Build
- Clone this repository.
- This project is dependent on LLVM 13. Follow the instructions in this
README.md
to download and build LLVM 13. - Navigate to the
compiler
directory. - Use
cargo
to build and test the project.cargo check
to check that the project compiles.cargo test
to compile the project and run its tests.