package rocq-equations
A function definition package for Rocq
Install
Dune Dependency
Authors
Maintainers
Sources
Coq-Equations-1.3.1-9.0.tar.gz
sha512=e8c4aa5b1ec4f9636b52047f0911c7bc7d3b69042011a626a8770866c7ca5f7cd722a45d62ff7ddf9903c4f295c7ca5cbe49f9e18f9675d55251f0e4c533306c
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: 20 Mar 2025
Dependencies (5)
-
ppx_optcomp
build - coq-core
- rocq-stdlib
-
ocaml
>= "4.10.0" -
dune
>= "3.13"
Dev Dependencies (3)
-
odoc
with-doc -
ocaml-lsp-server
with-dev-setup -
rocq-runtime
>= "9.0~" & < "9.1" & != "dev" & != "9.0.dev"
Used by (3)
-
coq-equations
>= "1.3.1+9.0" - rocq-hollight-logic
- rocq-hollight-logic-unif
Conflicts
None
On This Page