Reservoir

justinfargnoli/koi

Compiler for the Calculus of Inductive Constructions

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

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

  1. Clone this repository.
  2. This project is dependent on LLVM 13. Follow the instructions in this README.md to download and build LLVM 13.
  3. Navigate to the compiler directory.
  4. 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.