new summary syntax - 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

Closed garrigue closed 5 years ago

garrigue commented 5 years ago

Change

\rsum_(x # s , d) F x

into

\rsum_(x = d [~ s])

meaning x equal to d on the complement of s.

garrigue commented 5 years ago

Another possible syntax, but with a change of semantics, would be

\rsum_(x = d #> s) F x

meaning x equal to d on s (i.e. remove the implicit complement).

garrigue commented 5 years ago

I tried the other syntax, but while it nicely matches the sub_vec syntax (t # V), it doesn't work well with things like:

\rsum_(x = d #> ~:('V m0 :\ n0)) F x