package coq-infotheo

  1. Overview
  2. No Docs
Discrete probabilities and information theory for Coq

Install

Dune Dependency

github.com Edit opam file Versions (35)

Authors

  1. R
    Reynald Affeldt, AIST
  2. M
    Manabu Hagiwara, Chiba U. (previously AIST)
  3. J
    Jonas Senizergues, ENS Cachan (internship at AIST)
  4. Jacques Garrigue
  5. K
    Kazuhiko Sakaguchi, Tsukuba U.
  6. T
    Taku Asai, Nagoya U. (M2)
  7. T
    Takafumi Saikawa, Nagoya U.
  8. N
    Naruomi Obata, Titech (M2)
  9. A
    Alessandro Bruni, IT-University of Copenhagen

Maintainers

  1. R
    Reynald Affeldt <reynald.affeldt@aist.go.jp>

Sources

0.7.2.tar.gz
sha512=94aa64be13785c5622664ff5a8667c2806bddee47db38b6d645ed2a63627e0af1267aeebf52cd229936c541ef98d128e0b2c10a95251a64d8c75e9e7e3273ca8

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-06-27

Published: 27 Jun 2024

Dependencies (4)

  1. coq-interval >= "4.10.0"
  2. coq-mathcomp-algebra-tactics >= "1.2.0"
  3. coq-hierarchy-builder >= "1.5.0"
  4. coq-mathcomp-analysis (>= "1.2.0" & < "1.5.0")

Dev Dependencies (6)

  1. coq-mathcomp-field (>= "2.2.0") | (= "dev")
  2. coq-mathcomp-solvable (>= "2.2.0") | (= "dev")
  3. coq-mathcomp-algebra (>= "2.2.0") | (= "dev")
  4. coq-mathcomp-fingroup (>= "2.2.0") | (= "dev")
  5. coq-mathcomp-ssreflect (>= "2.2.0") | (= "dev")
  6. coq (>= "8.18" & < "8.20~") | (= "dev")

Used by (1)

  1. coq-monae = "0.0.2" | = "0.2.1" | = "0.7.0"

Conflicts

None