Coq ELPI

Coq-Elpi provides a Coq plugin that lets one define new commands and tactics in Elpi (Embeddable λProlog Interpreter). For that purpose it provides an embedding of Coq's terms into λProlog using the Higher-Order Abstract Syntax approach (HOAS). It also exports to Elpi a comprehensive set of Coq's primitives, so that one can print a message, access the environment of theorems and data types, define a new constant, declare implicit arguments, type classes instances, and so on. For convenience it also provides a quotation and anti-quotation for Coq's syntax, so that one can write {{ nat -> lp:X }} in the middle of a λProlog program instead of the equivalent AST prod `_` (global (indt «Coq.Init.Datatypes.nat»)) X.

Tags

coq prolog