package coq-monae
Monads and equational reasoning in Coq
Install
Dune Dependency
Authors
Maintainers
Sources
0.2.1.tar.gz
sha512=64763dadb87bd136ea6594eb5e615ed56d7e4d51d169a2254b9a70c11d1871251fa79b7822df469ec1bdfa2ae1e1530dc93bccb6d0298463901902d7af7bfa0f
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:monaePublished: 16 Dec 2020
Dependencies (8)
-
coq-paramcoq
>= "1.1.2" & < "1.2~" -
coq-infotheo
>= "0.2.1" -
coq-mathcomp-analysis
(= "0.3.4") -
coq-mathcomp-field
(>= "1.11.0" & < "1.12~") -
coq-mathcomp-solvable
(>= "1.11.0" & < "1.12~") -
coq-mathcomp-algebra
(>= "1.11.0" & < "1.12~") -
coq-mathcomp-fingroup
(>= "1.11.0" & < "1.12~") -
coq-mathcomp-ssreflect
(>= "1.11.0" & < "1.12~")
Dev Dependencies (1)
-
coq
(>= "8.11" & < "8.13~") | (= "dev")
Used by
None
Conflicts
None
On This Page