depsterr
/
implicitt
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
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.
23 Commits
1 Branch
0 Tags
597 KiB
 
Tag: Branch: Tree: master
Branches Tags
${ item.name }
Create tag ${ searchTerm }
Create branch ${ searchTerm }
from 'master'
${ noResults }
Rachel Samuelsson 7bc4be31c0
did some work on renaming / meta solutions 		4 months ago
bin started work on metas 4 months ago
lib did some work on renaming / meta solutions 4 months ago
.gitignore initial commit? 9 months ago
README.md started work on metas 4 months ago
dune-project initial commit? 9 months ago
implicitt.opam initial commit? 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)