Release 1.2 of Equations is available, as source and
coq-equations.1.2+8.10 for Coq 8.8 and Coq
8.9 and Coq 8.10beta1 (the later in the
I am pleased to announce release 1.2 of the Equations package. Equations is a function definition plugin for Coq, that supports the definition of functions by dependent pattern-matching and structural or well-founded, mutual or nested recursion and compiles them into core Coq terms without axioms. It automatically derives the clauses’ equations, the graph of the function and its associated elimination principle.
This release contains a few fixes and improvements with respect to the 1.2beta2 version:
Fixed an annoying backtracking bug when using
Equations?(issue #179, thanks to Pierre-Marie Pédrot for help fixing this).
Fixed the treatment of
withwith more than 2 arguments (issue #190)
Fixed “cannot be used as a hint” errors (issue #193), now turned into warnings.
Granted with #187: global
Set Equations Derive Equations/Eliminatoroptions.
The previous beta1 and beta2 announcements describe the new features of the 1.2 version. See the reference manual for up-to-date syntax and description of the new features. The Equations Reloaded paper also provides an introduction to the new version.
– Matthieu Sozeau