Documentation of Equations

What is Equations?

Equations is a function definition plugin for Coq, that allows the definition of functions by dependent pattern-matching and well-founded, mutual or nested structural recursion and compiles them into core terms. It automatically derives the clauses equations, the graph of the function and its associated elimination principle.

Documentation of Equations

• The Basics of Equations interactive version and source code
• Equations and Obligations interactive version and source code
• Equations and Well-founded Recursion interactive version and source code