kdrag.kernel.trigger
- kdrag.kernel.trigger(pf: Proof, patterns: list[ExprRef] = [], no_patterns: list[ExprRef] = []) Proof
Add e-matching triggers to a quantified proof. Logically speaking, does nothing.
>>> x,y = smt.Ints("x y") >>> p = kd.prove(smt.ForAll([x,y], y > 0, x + y > x)) >>> p.thm.num_patterns() 0 >>> p2 = trigger(p, patterns=[x + y]) >>> p2 |= ForAll([x, y], Implies(y > 0, x + y > x)) >>> p2.thm.pattern(0) Var(1) + Var(0)