package coq-equations
A function definition package for Coq
Install
Dune Dependency
Authors
Maintainers
Sources
v1.3-8.15.tar.gz
sha512=ec281fca0b148d9297f2c871a5485649bb93f24e8723f56a4a78d2bc6224984de16e0d6438fd3f7ee98ea0e69487208480bd44d3a30a92af667e38926b8dab0e
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: 19 Jan 2022
Dev Dependencies
None
Used by (10)
- coq-category-theory
-
coq-hydra-battles
>= "0.5"
- coq-katamaran
-
coq-metacoq-checker
= "1.0~alpha2+8.10" | = "1.0~beta1+8.11"
-
coq-metacoq-pcuic
!= "1.0~beta1+8.12" & < "1.0~beta2+8.12" | = "1.0+8.14" | = "1.1+8.14" | = "1.1.1+8.14"
-
coq-metacoq-template
>= "1.0~alpha2+8.10" & < "1.0~beta1+8.11" | >= "1.0~beta2+8.11" & < "1.2+8.16"
-
coq-metacoq-utils
!= "1.2.1+8.18" & < "1.3.1+8.18"
-
coq-monae
>= "0.4.1"
- coq-pil
-
coq-vlsm
>= "1.2"
Conflicts
None
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page