A dependently typed programming language with a very small core language. Try it out at https://atennapel.github.io/tinka
FEATURES:
- Type-in-type, not consistent, but type-safe
- Inductive-recursive datatypes using a functor fixpoint
- Erasure annotations
- Implicit parameters with type inference
TODO:
- add general indexed fixpoint type
- update libs to use fixpoint
- add heterogenous equality type with axiom K
- research inductive-recursive fixpoints
- implement inductive-recursive fixpoints
- test inductive-recursive fixpoints
- separate file/url references in syntax
- multi-line comments
- fix importing in web repl
- typed metas
- make sure metas solutions are correct with respect to erasure
- add primitive Nat
- add primitive Fin
- pruning and intersecting
- basic postponing
- fix issue with erasure in verification
- improve postponing
- fix negative vars in output
- have smarter way to verify meta solutions
- add syntax to explicitly reference local (debruijn)
- add codata fixpoint type
- add symbols and enumerations
- add testing
- fix case-insensitive filesystem support
- add surface syntax for modules
- add surface syntax for datatypes
- inductive-inductive fixpoints