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

prob interface #51

Open affeldt-aist opened 3 years ago

affeldt-aist commented 3 years ago

https://github.com/affeldt-aist/infotheo/blob/fdba7c47f758c2276c30b78bc35f69a279871527/lib/Reals_ext.v#L387

Since we're favoring a structure with an inequality in bool for prob, the constructor mk_ might turn out to be superfluous after all. Investigate its removal.

Cc: @t6s

t6s commented 3 years ago

~How about renaming closed to lt2W?~

NB(rei): has been taken care of by PR #52

t6s commented 3 years ago

~Oops this comment was not meant for this issue.~