Experimental Dependently Typed Programming Language
Features:
- Normalisation
- Type checking/inference
- Terms unification
- Inductive types
- Pattern matching
TO-DO:
- Implicit arguments
- Better syntax
- Higher inductive types
- Inductive type families
- More powerful universes
- Modules
Many things were reused from narc-rs project.