2023-01-26 21:13:51 +01:00
|
|
|
# implicitt (WIP)
|
2022-08-25 20:29:55 +02:00
|
|
|
|
2023-01-26 16:50:09 +01:00
|
|
|
A "proof assistant" with holes and implicit arguments. Developed to learn about elaboration, meta variables and OCaml
|
|
|
|
|
|
|
|
|
|
# Depends
|
|
|
|
|
|
|
|
|
|
* BNFC
|
|
|
|
|
* ocamlyacc
|
|
|
|
|
* ocamllex
|
2022-08-25 20:29:55 +02:00
|
|
|
|
|
|
|
|
# TODO
|
|
|
|
|
|
2023-01-31 19:51:46 +01:00
|
|
|
* 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?
|
|
|
|
|
|
2022-08-30 15:32:00 +02:00
|
|
|
* Raw syntax
|
2022-08-30 18:09:24 +02:00
|
|
|
* Parser (BNFC)
|
2022-08-30 15:32:00 +02:00
|
|
|
|
|
|
|
|
* Metas
|
2023-01-26 21:13:51 +01:00
|
|
|
* Holes
|
|
|
|
|
* Unification
|
2022-08-30 15:32:00 +02:00
|
|
|
* Implicit arguments
|
|
|
|
|
|
|
|
|
|
* More types
|
|
|
|
|
* Id
|
2023-01-26 21:13:51 +01:00
|
|
|
* W?
|
|
|
|
|
* Tarski Universes (in the core)?
|
|
|
|
|
|
|
|
|
|
* Pretty elimination syntax (cooltt esque)
|
