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 to MC2 #116

Closed gares closed 6 months ago

affeldt-aist commented 6 months ago

@gares Many thanks for having started that! I tried to make some progress.

fyi: @t6s @garrigue

gares commented 6 months ago

mixin naryChoice should not have a parameter (T : richType) but rather (T : Type) of Rich T.

affeldt-aist commented 6 months ago

@gares We are thinking about merging this one into master, that restricts the version of Mathcomp to >= 2.2.0