I wish theorem provers were more modular. As in, you could access the kernel proving language as a library, making it easier to provide a different frontend.
Conversation
Replying to
Maybe have a look at the DreamTT and CoolTT `Refiner` modules. These put the core language behind an API that can be accessed by an elaborator:
- github.com/jonsterling/dr
- github.com/RedPRL/cooltt/
I'm trying to learn more about the approach - it seems nifty and useful!