Rocq-Elpi
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
Rocq-Elpi
Index
Index