fact: Definition letter_pickle (l : letter) := match l with | Bit a => if a == (Zp0 : 'F_2) then O else 1%N | Star => 2%N | Blank => 3%N end.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext ssralg_ext num_occ f2 ssrR hamming tanner linearcode