kdrag.contrib.telescope.TForAll

kdrag.contrib.telescope.TForAll(xs: Telescope, P: BoolRef) → BoolRef

Dependent forall quantifier for a telescope of variables. Kind of like a proof irrelevant Pi type.

Subtype / Refinement style usage

>>> x, y, z = smt.Reals("x y z")
>>> TForAll([(x, x > 0), (y, y > x)], y > -1)
ForAll(x, Implies(x > 0, ForAll(y, Implies(y > x, y > -1))))

“Dependent type” style usage

>>> Pos = smt.Lambda([x], x > 0)
>>> GT = lambda x: smt.Lambda([y], y > x)
>>> TForAll([(x, Pos), (y, GT(x))], y > -1)
ForAll(x, Implies(x > 0, ForAll(y, Implies(y > x, y > -1))))

Parameters:

• xs (Telescope)

• P (BoolRef)

Return type:

BoolRef