You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
|
4 months ago | |
---|---|---|
bin | 4 months ago | |
lib | 4 months ago | |
.gitignore | 9 months ago | |
README.md | 4 months ago | |
dune-project | 9 months ago | |
implicitt.opam | 9 months ago |
README.md
implicitt (WIP)
A “proof assistant” with holes and implicit arguments. Developed to learn about elaboration, meta variables and OCaml
Depends
- BNFC
- ocamlyacc
- ocamllex
TODO
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)