kdrag.tele.DeclareFunction

kdrag.tele.DeclareFunction(name, tele0: Telescope, T: SubSort, by=[]) → FuncDeclRef

>>> x, y = smt.Ints("x y")
>>> Nat = smt.Lambda([x], x >= 0)
>>> GE = lambda x: smt.Lambda([y], y >= x)
>>> inc = DeclareFunction("inc", [(x, Nat)], GE(x))

Parameters:

• tele0 (Telescope)

• T (SubSort)

Return type:

FuncDeclRef