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

remove choice_of_Type #62

Closed affeldt-aist closed 2 years ago

affeldt-aist commented 3 years ago

https://github.com/affeldt-aist/infotheo/blob/1c6963020392898b945a2f84b42f620faa712a2a/probability/convex.v#L1100

it has been merged into MathComp-Analysis

affeldt-aist commented 3 years ago

as well as bigcup_of_singleton and bigcup_image

NB: bigcup_of_singleton became bigcup_imset1