package rocq-equations
A function definition package for Rocq
Install
Dune Dependency
Authors
Maintainers
Sources
v1.3.2-9.3.tar.gz
sha512=e007377a5cafaad39442fcccdf796bb88a5746505a8fe781e13271b6cce174a0cefe4f22c8f4b1ecf9945450d3554f44f5819c535892b05f0511758ab05d6d68
Description
Equations is a function definition plugin for Rocq, 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: 23 Oct 2026
Dependencies (4)
-
rocq-stdlib
>= "9.2.0~" -
rocq-core
>= "9.3~" & < "9.4~" -
ocaml
>= "4.10.0" -
dune
>= "3.13"
Dev Dependencies (2)
-
odoc
with-doc -
ocaml-lsp-server
with-dev-setup
Used by (10)
Conflicts
None
On This Page