saltt is a salt flavored type theory
Todo:
- Dependent types
- Bidirectional type checking
- Normalization by Evaluation
- Type in Type
- Meta variables, implict arugments and holes (pattern unification)
- Inductive data type and dependent pattern matching
- Coverage checking
- Record
- Prelude lib include Identity type, Nat, List, Bool, Bot, Top ... (using inductive data type)
- Mixfix operator definition (
if_then_else_) - Universe hierarchy (solve
Type : Type)
Long term goals:
- Agda's Typed Module System