search

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

define ereal_convType #75

Closed t6s closed 2 years ago

t6s commented 2 years ago

Finished defining ereal_convType, but with very unclean proofs. @affeldt-aist Could you take a glance at the changes?