Function random_linear_code_gv_ty 

pub fn random_linear_code_gv_ty() -> Expr

RandomLinearCodeGV : Nat → Nat → Prop — random linear codes over GF(q) achieve the Gilbert-Varshamov bound with high probability.