kdrag.tele.ann

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

Annotate an expression with a type.

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

Parameters:

• x (ExprRef)

• T (SubSort)

Return type:

ExprRef