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