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

Generalize fdists #99

Closed Tragicus closed 1 year ago

Tragicus commented 1 year ago

fdists are currently defined over the R type of the standard library. Some developments would like to rely on this library but use structures from the mathcomp library. So we would like to have them generalized (maybe to numFieldType).

affeldt-aist commented 1 year ago

Indeed, with a generalization akin to this one: https://github.com/affeldt-aist/trajectories/blob/d4da32f8ca7dbff1ad8ef1aafa5071dba5218d6a/theories/hulls.v#L16-L45

affeldt-aist commented 1 year ago

PR #103 does that and should be merged very soon into master.