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

avoid Program Definition at bseq0; canonicize bseq0 #14

Closed t6s closed 4 years ago

t6s commented 4 years ago

The definition of bseq0 in master uses Program Definition, which is however unnecessary and complicates the term. This commit avoids it.

Additionally bseq0 is declared Canonical to allow the expression [bseq of [::]].