package coq-equations
A function definition package for Coq
Install
Dune Dependency
Authors
Maintainers
Sources
v1.2.3-8.12.tar.gz
sha512=c19617ef127a56916d67b2c347f21cd267b250a23988424bb1486336e784a5df7a6c85ee355eb99e148431f8d7b3534993f3fdba3aaa4769d74f8c3548fb2efa
Description
Equations is a function definition plugin for Coq, that allows the definition of functions by dependent pattern-matching and well-founded, mutual or nested structural recursion and compiles them into core terms. It automatically derives the clauses equations, the graph of the function and its associated elimination principle.
Tags
keyword:dependent pattern-matching keyword:functional elimination category:Miscellaneous/Coq Extensions logpath:EquationsPublished: 30 Jul 2020
Dependencies (1)
-
coq
>= "8.12.0" & < "8.13~"
Dev Dependencies
None
Used by (9)
- coq-category-theory
- coq-hydra-battles
-
coq-katamaran
< "0.2.0"
-
coq-library-undecidability
< "1.0.1+8.16"
-
coq-metacoq-checker
= "1.0~alpha2+8.10" | >= "1.0~beta1+8.11"
-
coq-metacoq-pcuic
< "1.0+8.14"
-
coq-metacoq-template
>= "1.0~alpha2+8.10" & < "1.0~beta1+8.11" | >= "1.0~beta2+8.11" & < "1.0+8.14"
- coq-pil
-
coq-vlsm
>= "1.2"
Conflicts
None
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page