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)

Maintainers

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

Sources

0.2.2.tar.gz
sha512=dc447af837732867e046afaf56feca3d73cdad0e25b6b24abb2fa45a4c9a78b2a67f508150418e122976bdd9828f3058e47f8aa8c7dca65243be527f3da96ec3

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 logpath:infotheo

Published: 07 Jan 2021

Dependencies (6)

  1. coq-mathcomp-analysis (>= "0.3.4" & < "0.3.8")
  2. coq-mathcomp-field (>= "1.12.0" & < "1.13~")
  3. coq-mathcomp-solvable (>= "1.12.0" & < "1.13~")
  4. coq-mathcomp-algebra (>= "1.12.0" & < "1.13~")
  5. coq-mathcomp-fingroup (>= "1.12.0" & < "1.13~")
  6. coq-mathcomp-ssreflect (>= "1.12.0" & < "1.13~")

Dev Dependencies (1)

  1. coq (>= "8.11" & < "8.13~") | (= "dev")

Used by (1)

  1. coq-monae = "0.0.2" | >= "0.2" & < "0.3"

Conflicts

None