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

rename constructor #41

Closed affeldt-aist closed 3 years ago

affeldt-aist commented 3 years ago

https://github.com/affeldt-aist/infotheo/blob/289821f43bd28ffc98b7faaac00828343cd8ef3e/probability/convex.v#L1101

Should be Mixin @t6s