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
repository: http://github.com/mattam82/Coq-Equations.
Equations: A Dependent Pattern-Matching Compiler. Matthieu Sozeau, Talk given at PPS - Université Paris 7, January 2010.
Equations: A Dependent Pattern-Matching Compiler in First International Conference on Interactive Theorem Proving. Matthieu Sozeau. Springer, July 2010.
Valid XHTML 1.1! Valid CSS!