Dist necset notation - Githubissues

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

Dist necset notation #49

Closed affeldt-aist closed 3 years ago

affeldt-aist commented 3 years ago

@t6s

t6s commented 3 years ago

For necset, can you make the notation convey not only convType but semiCompSemiLattConvType structure?

Definition Necset_of (A : convType) :=
  fun phT : phant (Choice.sort A) => necset_semiCompSemiLattConvType A.
Notation "{ 'necset' T }" := (Necset_of (Phant T)) : convex_scope.

If possible, would there be any drawbacks?

affeldt-aist commented 3 years ago

If possible, would there be any drawbacks?

Not that I see right now.

t6s commented 3 years ago

I approve this PR unless the ongoing CI fails.