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

port of infotheo to HB #83

Closed affeldt-aist closed 2 years ago

affeldt-aist commented 2 years ago

@t6s could you take a quick look at the documentation while the changes are still fresh in our minds? :-)

affeldt-aist commented 2 years ago

@CohenCyril @gares We had a small hierarchy of structures about convexity that we have ported from hand-made packed classes to HB. We thought that you might be interested in the diff.