kdrag.rewrite.rw_trig

kdrag.rewrite.rw_trig(e: Proof, rev=False) → Proof

Take a rewrite rule and add triggers to it for the lhs or rhs

>>> x = smt.Int("x")
>>> pf = kd.prove(smt.ForAll([x], x + 1 == 1 + x))
>>> pf2 = rw_trig(pf)
>>> pf2
|= ForAll(X!..., X!... + 1 == 1 + X!...)
>>> pf2.thm.pattern(0)
Var(0) + 1
>>> rw_trig(pf,rev=True).thm.pattern(0)
1 + Var(0)

Parameters:: e (Proof)
Return type:: Proof