A “proof assistant” with holes and implicit arguments. Being developed to learn about elaboration, meta variables and OCaml.
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.
 
 
Rachel Samuelsson 2c380ad564 remove old parse dir 1 week ago
bin I hate grammers 5 months ago
lib remove old parse dir 1 week ago
.gitignore initial commit? 5 months ago
README.md initial post process 1 week ago
dune-project initial commit? 5 months ago
implicitt.opam initial commit? 5 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

  • Raw syntax

    • Parser (BNFC)
  • Metas

    • Holes
    • Unification
  • Implicit arguments

  • More types

    • Id
    • W?
    • Tarski Universes (in the core)?
  • Pretty elimination syntax (cooltt esque)