kdrag.rewrite.rewrite_of_expr

kdrag.rewrite.rewrite_of_expr(thm: BoolRef | QuantifierRef | Proof) → RewriteRule

Unpack theorem of form forall vs, lhs = rhs into a Rule tuple

>>> x = smt.Real("x")
>>> rewrite_of_expr(smt.ForAll([x], x**2 == x*x))
RewriteRule(vs=[X...], lhs=X...**2, rhs=X...*X...)