dreamtt
dreamtt copied to clipboard
jonsterling
A pedagogic implementation of abstract bidirectional elaboration for dependent type theory.
- https://github.com/RedPRL/cooltt/blob/master/src/core/TermBuilder.mli - https://github.com/RedPRL/cooltt/blob/master/src/core/Splice.mli
https://github.com/RedPRL/cooltt/blob/master/src/core/Tactic.ml#L95
I created this PR for WIP frontend. * [x] A dummy driver * [ ] Some grammar stuff
Right now, this is only an elaborator; there is no notion of top-level declaration, and no parser.
Metadata
Owner
Metadata
A pedagogic implementation of abstract bidirectional elaboration for dependent type theory.