unnecessary Require Import - Githubissues

affeldt-aist / infotheo

A Coq formalization of information theory and linear error-correcting codes

GNU Lesser General Public License v2.1

64 stars 15 forks source link

unnecessary Require Import #18

Closed affeldt-aist closed 4 years ago

affeldt-aist commented 4 years ago

https://github.com/affeldt-aist/infotheo/blob/de840710dde1127534875952bd941331c01fcf1c/probability/convex_choice.v#L1942