This is an implementation of a type theory (Cedille) with syntactic metaprogramming. Essential features and syntax of the language are built in itself via metaprogramming. This includes things such as the module system, datatype system and type inference. The preprint contains a fairly complete theoretical description of the system, and the wiki and blog contain some additional information and documentation.
Building with nix is the only setup that’s actively maintained. Any other setup may or may not be broken.
- Using Nix
If you have installed nix, simply run nix-build. Alternatively, running install.sh will build and install the executable to the system.
- Manually
Agda 2.6.2, the Agda standard library (version 1.7), bytestring-trie and containers (the Haskell libraries) are required. If those are setup correctly, just use the makefile. If you are using stack, you can also try make stack (this will not install Agda and the Agda standard library for you though).
The file mced/Test.mced contains the current tests. Run meta-cedille --load Test in the mced directory to execute all current tests.