Rocq-Elpi

Rocq-Elpi embeds Elpi, an implementation of λProlog, into the Rocq prover. It lets one write commands, tactics, and even entire plugins in a logic programming language well suited to manipulate the abstract syntax trees of Rocq terms, including binders and unification variables.

The Elpi user manual is a separate document: this manual only gives a short tutorial on Elpi itself, and defers to it for the full language reference.

Tutorials

• Getting started
• The Elpi programming language
• HOAS for Rocq terms
• Writing commands in Elpi
• Polishing a command
• Writing tactics in Elpi
• More tactic examples and the proof engine
• Adding builtin predicates via an OCaml plugin

Reference

• Vernacular commands
• Separation of parsing from execution
• Invocation of Elpi code
• Builtins and relevant files

Examples

• Examples

Applications

• Applications written in Rocq-Elpi