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

change the notation for tnth from \_ to avoid a conflict with mca #110

Closed t6s closed 10 months ago

t6s commented 10 months ago

The notation \_ for tnth defined in ssr_ext.v (at level 9) conflicts with the one in classical_sets (at level 10), blocking uses of mathcomp-analysis at some places, particularly when trying to reboot PR #67 .

This PR replaces it by \__ (one extra underscore) to avoid the conflict.

t6s commented 10 months ago

I also noticed a few lemmas marked in bayes.v to be moved to ssr_ext.v, and did it.

affeldt-aist commented 10 months ago

This is fine with me. Have you considered other notations of less than 3 characters? Maybe !_ could have worked. It looks like array addressing to me, which seems appropriate here. (This could even be proposed at the MathComp level.)

affeldt-aist commented 10 months ago

This is fine with me. Have you considered other notations of less than 3 characters? Maybe !_ could have worked. It looks like array addressing to me, which seems appropriate here. (This could even be proposed at the MathComp level.)

Haskell is using ! for array subscripting by the way.

t6s commented 10 months ago

This is fine with me. Have you considered other notations of less than 3 characters? Maybe !_ could have worked. It looks like array addressing to me, which seems appropriate here. (This could even be proposed at the MathComp level.)

No, and I have no particular preference. Which do you really like?

affeldt-aist commented 10 months ago

in the circumstances, !_ looks appropriate

t6s commented 10 months ago

looks pretty enough