search

Andromedans / andromeda

A proof assistant for general type theories
http://www.andromeda-prover.org/
Other
298 stars 35 forks source link

Become a Coq plugin? #384

Open SkySkimmer opened 6 years ago

SkySkimmer commented 6 years ago

@TheoWinterhalter has a translation from ETT with annotations on applications to ITT + K + funext. We could use this to produce ITT terms when we have a judgment. We could then throw those terms at another tool like Coq.

TheoWinterhalter commented 6 years ago

What would be the benefit of becoming a Coq plugin rather than just building a bridge between andromeda and Coq?

For reference, the repository is https://github.com/TheoWinterhalter/ett-to-itt.

JasonGross commented 6 years ago

Ooh, would this let me use andromeda as a DSL in Coq, and use tactics to do things with Andromeda terms?