package rocq-monae
Monads and equational reasoning in Rocq
Install
Dune Dependency
Authors
Maintainers
Sources
0.9.2.tar.gz
sha512=c4ab455a457b2e92c3d2df72a29434a3e6e17395dadbfb291e51392dc5f7ba6b5fd90e1120fd93b47935916685f2b5ae08d8ba138e04187e2a2c3ab6c000963f
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-04-07Published: 21 Apr 2026
Dependencies (11)
-
rocq-equations
>= "1.3" & < "1.4~" -
rocq-hierarchy-builder
>= "1.9.1" -
rocq-elpi
>= "3.3.0" -
coq-infotheo
>= "0.9.7" -
coq-mathcomp-analysis
>= "1.12.0" -
rocq-mathcomp-field
>= "2.4.0" -
rocq-mathcomp-solvable
>= "2.4.0" -
rocq-mathcomp-algebra
>= "2.4.0" -
rocq-mathcomp-fingroup
>= "2.4.0" -
rocq-mathcomp-ssreflect
>= "2.4.0" -
rocq-core
(>= "9.0" & < "9.1~")
Dev Dependencies
None
Used by (1)
-
coq-monae
>= "0.9.2"
Conflicts
None
On This Page