coq-equations 1.2.1 Function definition plugin for Coq
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.
- Website: https://mattam82.github.io/Coq-Equations/
- License: LGPL 2.1
- Package source: coq.scm
- Patches: None
- Builds: x86_64-linux, i686-linux