Toy implementation of the calculus of (inductive) constructions.
Usage: mu [-i] [-v] [-h] [<file>]
| option | meaning |
|---|---|
-v |
verbose mode, report all definitions from files |
-i |
interactive mode, start REPL after executing <file> |
-h |
show help |
<file> |
muprov file to run. if no file is given, a REPL is started. |
The REPL can optionally make use of the readline package if it is installed.
LuaJIT is supported.
base.mu contains some basic data types and functions.
The theorems directory contains proofs for some example theorems.
The bugs directory contains test files for various bugs that have either been fixed or will be fixed in the future.
Type universes are TODO. This means that right now the logic is inconsistent, since type-in-type allows for paradoxes. See bugs/hurkens.mu for an implementation of Hurken's paradox.
Some helpful papers used: