kdrag.rewrite.rewrite_of_expr_exact

kdrag.rewrite.rewrite_of_expr_exact(pf: ExprRef | Proof) → RewriteRule | None

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

>>> x = smt.Real("x")
>>> rewrite_of_expr_exact(smt.ForAll([x], x**2 == x*x))
RewriteRule(vs=[X...], lhs=X...**2, rhs=X...*X...)
>>> assert rewrite_of_expr_exact(x**2 == x + 1) is None

Parameters:

pf (ExprRef | Proof)

Return type:

RewriteRule | None