(WIP) a Proof Assistant written in Moonbit. Now it is just a NbE based bidirectional type checker for MLTT.
- STLC
- Unit type
- Π type
- Σ type
- Id type
- J eliminator
- W type
- Universe Hierarchy
- Contravariant Subtyping for Pi-types
Towards a practical programming language based on dependent type theory
A tutorial implementation of a dependently typed lambda calculus
[Chinese] Luna Flow QQ group: 762311556
[English/Japanese/Chinese] Email: zhehao0827 at 163.com