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

vandermonde to MathComp #69

Closed affeldt-aist closed 6 months ago

affeldt-aist commented 3 years ago

https://github.com/affeldt-aist/infotheo/blob/56a667c1421a9eb7a62593512a609711c0938f4f/lib/vandermonde.v#L8

this should be cleaned and PRed to MathComp...

affeldt-aist commented 2 years ago

NB: wip by @yoshihiro503

affeldt-aist commented 2 years ago

See https://github.com/math-comp/math-comp/pull/937

affeldt-aist commented 1 year ago

We should now remove it and use MathComp instead.