package coq-infotheo
- Overview
- No Docs
You can search for identifiers within the package.
in-package search v0.2.0
Discrete probabilities and information theory for Coq
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.7.6.tar.gz
sha512=60811b68caba4e575fc93afa4db7a191c17eb378b90972d10e8fb97d29be2a4ccf2f25eece1af2fb325636cc68597962040aea5818f56c6b610307daf2bccc3e
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:2024-12-19Published: 19 Dec 2024
Dependencies (10)
-
coq-interval
>= "4.10.0" -
coq-mathcomp-algebra-tactics
>= "1.2.0" -
coq-hierarchy-builder
(>= "1.5.0" & < "1.8.0") -
coq-mathcomp-reals-stdlib
(>= "1.7.0") -
coq-mathcomp-analysis
(>= "1.7.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 (1)
-
coq-monae
= "0.0.2" | = "0.2.1" | >= "0.7.0"
Conflicts
None
On This Page