Copyright 2009-2017 Matthieu Sozeau matthieu.sozeau@inria.fr
Copyright 2015-2017 Cyprien Mangin cyprien.mangin@m4x.org

Distributed under the terms of the GNU Lesser General Public License Version 2.1 (see LICENSE for details).

Equations provides a notation for writing programs by dependent pattern-matching and (well-founded) recursion in Coq. It compiles everything down to eliminators for inductive types, equality and accessibility, providing a definitional extension to the Coq kernel.

The reference manual providing an introduction is available along with examples.

Two articles describing the system are available:

• Equations Reloaded, Cyprien Mangin and Matthieu Sozeau (October 2017). Submitted.
• Equations: A Dependent Pattern-Matching Compiler Matthieu Sozeau (2010) In: Kaufmann M., Paulson L.C. (eds) Interactive Theorem Proving. ITP 2010. Lecture Notes in Computer Science, vol 6172. Springer, Berlin, Heidelberg.

The current development version works with Coq 8.6 (branch master) and Coq 8.7 (branch 8.7), see releases for sources.

This package is available on OPAM. Activate the Coq repository if you didn't do it yet:

opam repo add coq-released https://coq.inria.fr/opam/released

and run:

opam install coq-equations

To get the beta versions of Coq, activate the repository:

opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev

To get the development version of Equations, activate the repository:

opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev

Alternatively, to compile Equations, simply run:

coq_makefile -f _CoqProject -o Makefile
make

in the toplevel directory, with coqc and ocamlc in your path.

Then add the paths to your .coqrc:

Add ML Path "/Users/mat/research/coq/equations/src".
Add Rec LoadPath "/Users/mat/research/coq/equations/theories" as Equations.

Or install it:

make install

As usual, you will need to run this command with the appropriate privileges if the version of Coq you are using is installed system-wide, rather than in your own directory. E.g. on Ubuntu, you would prefix the command with sudo and then enter your user account password when prompted.