kdrag.tele.open_binder

kdrag.tele.open_binder(e: BoolRef, n: int = 100000) → tuple[_Tele, BoolRef]

Open a formula in telescope form forall x, P(x), forall y, Q(y), R

>>> x, y = smt.Ints("x y")
>>> open_binder(TForAll([(x, x > 0), (y, y > 0)], x == y))
([(X!..., X!... > 0), (Y!..., Y!... > 0)], X!... == Y!...)
>>> open_binder(TForAll([(x, x > 0), (y, y > 0)], x == y), n=1)
([(X!..., X!... > 0)], ForAll(y, Implies(y > 0, X!... == y)))

Parameters:

• e (BoolRef)

• n (int)

Return type:

tuple[_Tele, BoolRef]