kdrag.tele.Pi

kdrag.tele.Pi(tele0: Telescope, B: SubSort) → SubSort

Multiarity Pi. Dependent Function subsort B is a family because it may include parameters from tele0.

>>> x, y = smt.Ints("x y")
>>> GE = lambda x: smt.Lambda([y], y >= x)
>>> Pi([(x, Nat)], GE(x))
Lambda(f!...,
    ForAll(x, Implies(x >= 0, Lambda(y, y >= x)[f!...[x]])))
>>> smt.simplify(Pi([(x, Nat)], GE(x))[smt.Lambda([x], x)])
True

Parameters:

tele0 (Telescope)
B (SubSort)

Return type:

SubSort