Welcome to Equations-Fpred

Matthieu Sozeau and Cyprien Mangin

New, without the JMeq_eq axiom

Packages for opam working with the current 8.5 development branch are available. You need to install opam using the repositories available at: coq-opam-archive, see the README there for instructions. Then simply:

opam install coq:equations-fpred
You can have a look at the documented sources here.

Old

Here is a tarball of the formalization: equations-fpred-1.0.0.tgz and HTML documentation.

You currently need the current v8.5 branch of the git of Coq on github (tested with commit df54c829a4c06a93de47df4e8ccc441721360da8), along with the Equations 8.5 branch (tested with commit fad10a411c7b101fb514140689a83110a87304bd), and this version of CoLoR to compile the whole development (make; make install for both).