package rocq-equations
A function definition package for Rocq
Install
Dune Dependency
Authors
Maintainers
Sources
v1.3.2-9.2.tar.gz
sha512=04fb7a776b5ef6c3e34d8bdb9fe5e8873b03bff5616ae563eccba4121ad92bb2f49c9a8e2f178cb168ba71426c6ee1ac9f8dee72107dad62923c9006f03fbb9e
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: 08 Jun 2026
Dependencies (6)
-
ppx_optcomp
build -
rocq-stdlib
>= "9.1.0~" -
coq-core
>= "9.2~" -
rocq-core
>= "9.2~" & < "9.3~" -
ocaml
>= "4.10.0" -
dune
>= "3.13"
Dev Dependencies (2)
-
odoc
with-doc -
ocaml-lsp-server
with-dev-setup
Used by (6)
Conflicts
None
On This Page