kdrag.rewrite.horn_trig

kdrag.rewrite.horn_trig(e: Proof) → Proof

Take a horn clause and add triggers to it for the head

>>> x = smt.Int("x")
>>> pf = kd.prove(smt.ForAll([x], x > 0, x >= 0))
>>> pf2 = horn_trig(pf)
>>> pf2
|= ForAll(X!..., Implies(X!... > 0, X!... >= 0))
>>> pf2.thm.pattern(0)
Var(0) >= 0

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