kdrag.contrib.telescope.TExists

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

Dependent exists quantifier for a telescope of variables. Kind of like a proof irrelevant Sigma type.

Subtype / Refinement style usage

>>> x, y, z = smt.Reals("x y z")
>>> TExists([(x, x > 0), (y, y > x)], y > -1)
Exists(x, And(x > 0, Exists(y, And(y > x, y > -1))))

“Dependent type” style usage

>>> Pos = smt.Lambda([x], x > 0)
>>> GT = lambda x: smt.Lambda([y], y > x)
>>> TExists([(x, Pos), (y, GT(x))], y > -1)
Exists(x, And(x > 0, Exists(y, And(y > x, y > -1))))

Parameters:

xs (Telescope)
P (BoolRef)

Return type:

BoolRef