kdrag.tele.ann

kdrag.tele.ann(x: ExprRef, T: SubSort) → ExprRef

Annotate an expression with a type.

>>> x = smt.Int("x")
>>> Nat = smt.Lambda([x], x >= 0)
>>> ann(x, Nat)
ann(x, Lambda(x, x >= 0))

Parameters:

Return type:

ExprRef