package coq-infotheo
Discrete probabilities and information theory for Rocq
Install
Dune Dependency
Authors
-
RReynald Affeldt, AIST
-
MManabu Hagiwara, Chiba U. (previously AIST)
-
JJonas Senizergues, ENS Cachan (internship at AIST)
-
Jacques Garrigue
-
KKazuhiko Sakaguchi, Tsukuba U.
-
TTaku Asai, Nagoya U. (M2)
-
TTakafumi Saikawa, Nagoya U.
-
NNaruomi Obata, Titech (M2)
-
AAlessandro Bruni, IT-University of Copenhagen
Maintainers
Sources
0.9.7.tar.gz
sha512=1f058fe0732e335c4c73147750b22f281e8bff2fbfe79569be7d49781bfeb6d41b9360dedc7f63904fcabdf218e88a80dda712854a37456ccdb79a814b3915b8
Description
Infotheo is a Rocq 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:2026-03-05Published: 05 Mar 2026
Dependencies (14)
-
coq-interval
>= "4.10.0" -
coq-mathcomp-algebra-tactics
>= "1.2.6" -
coq-elpi
>= "3.0.0" -
coq-hierarchy-builder
>= "1.10.0" -
coq-elpi
< "3.0.0" -
coq-hierarchy-builder
= "1.9.1" -
coq-mathcomp-reals-stdlib
(>= "1.12.0") -
coq-mathcomp-analysis
(>= "1.12.0") - coq-mathcomp-field
- coq-mathcomp-solvable
- coq-mathcomp-algebra
- coq-mathcomp-fingroup
-
coq-mathcomp-ssreflect
(>= "2.4.0" & < "2.7~") -
coq
(>= "9.0" & < "9.2~")
Dev Dependencies
None
Used by (2)
-
coq-monae
= "0.0.2" | = "0.2.1" | >= "0.7.0" & < "0.9.2" - rocq-monae
Conflicts
None
On This Page