# 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)