kdrag.rewrite.rule_of_expr_exact
- kdrag.rewrite.rule_of_expr_exact(pf: ExprRef | Proof) Rule | None
Unpack _exactly_ theorem of form forall vs, body => head into a Rule tuple
>>> x = smt.Real("x") >>> rule_of_expr_exact(smt.ForAll([x], smt.Implies(x**2 == x*x, x > 0))) Rule(vs=[X...], hyp=X...**2 == X...*X..., conc=X... > 0, pf=None) >>> assert rule_of_expr_exact(x > 0) is None