32 lines
547 B
Markdown
32 lines
547 B
Markdown
# 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)
|