pub fn cry_ext_linear_code_ty() -> Expr
LinearCode : Nat → Nat → Nat → Type
A linear error-correcting code [n, k, d]: a k-dimensional subspace of F_2^n with minimum Hamming distance d. Can correct up to ⌊(d-1)/2⌋ errors.