Equations: A Dependent Pattern-Matching Compiler. Matthieu Sozeau, Talk given at PPS - Université Paris 7, January 2010.
Equations
Equations is a plugin for Coq implementing a dependent
pattern-matching compiler and a set of tools generating
support proofs for these definitions.
I presented the prototype
[1]
and a paper describes the features and the implementation of the
tool [2].
A very
preliminary tutorial
is available too.
The code is available through a
git
repository:
http://github.com/mattam82/Coq-Equations.