package rocq-monae
Monads and equational reasoning in Rocq
Install
Dune Dependency
Authors
Maintainers
Sources
0.9.3.tar.gz
sha512=5597cd91d798ffd63ccaf74fac0279598df7751047dbccd3ba0480ccea61cfab07d6b8c608cc0d16d27243f52cbd181f6c59b6649080bd8dd0f8931ef3266cd2
Description
This Rocq library contains a hierarchy of monads with their laws used in several examples of monadic equational reasoning.
Tags
keyword:monae keyword:effects keyword:probability keyword:nondeterminism logpath:monae date:2026-09-22Published: 28 Sep 2026
Dependencies (8)
-
rocq-mathcomp-zify
>= "1.7~" -
rocq-equations
>= "1.3" & < "1.4~" -
rocq-hierarchy-builder
>= "1.10" -
rocq-elpi
>= "3.5.0" -
rocq-infotheo
>= "0.9.8" -
rocq-mathcomp-analysis
>= "1.18.0" -
rocq-core
(>= "9.1" & < "9.3~") -
coq
>= "9.1" & < "9.4~"
Dev Dependencies
None
Used by
None
Conflicts
None
On This Page