package coq-monae
Monads and equational reasoning in Coq
Install
Dune Dependency
Authors
Maintainers
Sources
0.9.0.tar.gz
sha512=aa7ac3fd5fec110cf17ec1f054ff23d3f7ccbbd82a29fece0d18000c2829fc84746580c3229c9aaa633ca9d0338824823826af2a34494774d2374999f6bcb19b
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.theories logpath:monaeImpredicativeSet date: 2025-02-26Published: 26 Feb 2025
Dependencies (10)
-
coq-equations
>= "1.3" & < "1.4~" -
coq-hierarchy-builder
>= "1.7.0" -
coq-paramcoq
>= "1.1.3" & < "1.2~" -
coq-infotheo
>= "0.9.1" -
coq-mathcomp-analysis
(>= "1.9.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")
Dev Dependencies (1)
-
coq
(>= "8.19" & < "8.21~") | (= "dev")
Used by
None
Conflicts
None
On This Page