Release 1.2 of Equations is available, as source and through opam packages coq-equations.1.2+8.8, coq-equations.1.2+8.9, coq-equations.1.2+8.10 for Coq 8.8 and Coq 8.9 and Coq 8.10beta1 (the later in the extra-dev repository).

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 with with 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/Eliminator options.

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