kdrag.notation.QLambda

kdrag.notation.QLambda(xs: list[ExprRef], *args)

Conditional Lambda. If conjunction of conditions are not met, returns unconstrained value.

>>> x = smt.Int("x")
>>> QLambda([x], x > 0, x + 1)
Lambda(x, If(x > 0, x + 1, f!...(x)))
>>> QLambda([x], x > 0, x < 10, x + 1)
Lambda(x, If(And(x > 0, x < 10), x + 1, f!...(x)))

Parameters:

xs (list[ExprRef])