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