implicitt (WIP)

A “proof assistant” with holes and implicit arguments. Developed to learn about elaboration, meta variables and OCaml

Depends

Figure out representation of metas
- Types needed for stuck values and typed conversion
- Meta has value or other meta for type?
- Where to put this file?
Raw syntax
- Parser (BNFC)
Metas
- Holes
- Unification
Implicit arguments
More types
- Id
- W?
- Tarski Universes (in the core)?
Pretty elimination syntax (cooltt esque)