package coq-infotheo
Discrete probabilities and information theory for Coq
Install
Dune Dependency
Authors
Maintainers
Sources
0.3.8.tar.gz
sha512=d4163f4065418719c26c5bfd773482d63a2033d5bacc67bff5390ff8f28bbf45d53cc78d3e0cc9006480cc5f8a307062fdb8b9c26f698f5035f2f2bdd2e3b920
Description
Infotheo is a Coq library for reasoning about discrete probabilities, information theory, and linear error-correcting codes.
Tags
keyword:information theory keyword:probability keyword:error-correcting codes keyword:convexity logpath:infotheo date:2022-08-24Published: 24 Aug 2022
Dependencies (1)
-
coq-mathcomp-analysis
(>= "0.5.3") & (< "0.6~")
Dev Dependencies (6)
-
coq-mathcomp-field
(>= "1.13.0" & < "1.16~") | (= "dev") -
coq-mathcomp-solvable
(>= "1.13.0" & < "1.16~") | (= "dev") -
coq-mathcomp-algebra
(>= "1.13.0" & < "1.16~") | (= "dev") -
coq-mathcomp-fingroup
(>= "1.13.0" & < "1.16~") | (= "dev") -
coq-mathcomp-ssreflect
(>= "1.13.0" & < "1.16~") | (= "dev") -
coq
(>= "8.14" & < "8.16~") | (= "dev")
Used by (1)
-
coq-monae
= "0.0.2" | = "0.2.1" | >= "0.3.2" & != "0.4" & < "0.4.3"
Conflicts
None
On This Page