kdrag.tactics.forallI

kdrag.tactics.forallI(e: QuantifierRef, cb: Callable[[BoolRef, ExprRef], Proof]) → Proof

Open a forall quantifier but giving a new goal and fresh variables to a callback function.

>>> x = smt.Int("x")
>>> forallI(smt.ForAll([x], x > x - 1), lambda goal, x1: kd.prove(goal))
|- ForAll(x, x > x - 1)

Parameters:

Return type:

Proof