`necset_convType ` defines its own convex combination operation, while it should reuse `conv_set`

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

`necset_convType ` defines its own convex combination operation, while it should reuse `conv_set` #44

Closed t6s closed 3 years ago

t6s commented 3 years ago

The definitions of conv_set and the convex operation for necset_convType are essentially the same. We should prepare more lemmas for conv_set and make necset_convType rely on them.

(I'm working on this issue in conv_set branch.)