Package coq-elpi.1.19.2

[coqelpibot]

coq-elpi.1.19.2

Elpi extension language for Coq
Coq-elpi provides a Coq plugin that embeds ELPI.
It also provides a way to embed Coq's terms into λProlog using
the Higher-Order Abstract Syntax approach
and a way to read terms back. In addition to that it exports to ELPI a
set of Coq's primitives, e.g. printing a message, accessing the
environment of theorems and data types, defining a new constant and so on.
For convenience it also provides a quotation and anti-quotation for Coq's
syntax in λProlog. E.g. {{nat}} is expanded to the type name of natural
numbers, or {{A -> B}} to the representation of a product by unfolding
the -> notation. Finally it provides a way to define new vernacular commands
and
new tactics.

---

• Homepage: https://github.com/LPCIC/coq-elpi
• Source repo: git+https://github.com/LPCIC/coq-elpi
• Bug tracker: https://github.com/LPCIC/coq-elpi/issues

---

🐫 Pull-request generated by opam-publish v2.0.3