package coq-monae
Monads and equational reasoning in Coq
Install
Dune Dependency
Authors
Maintainers
Sources
0.9.1.tar.gz
sha512=5abde546b8e22ce9d0288eb45b5f095d4c019cb285a442c76d5da8bf1da5e38df89865c906083cc51e4754bc0d094c142a51d1b68e5706437a65f7a6b03cb08b
Description
This Coq 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:2025-07-19Published: 23 Jul 2025
Dependencies (11)
-
coq-equations
>= "1.3" & < "1.4~" -
coq-hierarchy-builder
(>= "1.8.0") -
coq-paramcoq
>= "1.1.3" & < "1.2~" -
coq-infotheo
>= "0.9.3" -
coq-mathcomp-analysis
(>= "1.11.0") -
coq-mathcomp-field
(>= "2.3.0") -
coq-mathcomp-solvable
(>= "2.3.0") -
coq-mathcomp-algebra
(>= "2.3.0") -
coq-mathcomp-fingroup
(>= "2.3.0") -
coq-mathcomp-ssreflect
(>= "2.3.0") -
coq
(>= "8.19" & < "8.21~")
Dev Dependencies
None
Used by
None
Conflicts
None
On This Page