Function hamming_code_optimal_ty 

pub fn hamming_code_optimal_ty() -> Expr

HammingCodeOptimal : Nat → Prop — Hamming codes are the unique perfect single-error-correcting codes (up to equivalence).