kdrag.tele.define

kdrag.tele.define(name: str, args: Telescope, T: SubSort, body: ExprRef, by=None, **kwargs) → FuncDeclRef

Define a function with a precondition given by a telescope of arguments and a postcondition given by a subset that output will lie in.

Automatically

>>> n = kd.kernel.FreshVar("n", smt.IntSort())
>>> m = smt.Int("m")
>>> Nat = smt.Lambda([n], n >= 0)
>>> Pos = smt.Lambda([n], n > 0)
>>> inc = define("test_inc", [(n,Nat)], Pos, n + 1)
>>> inc.pre_post
|= ForAll(n!...,
    Implies(And(n!... >= 0),
        Lambda(n!..., n!... > 0)[test_inc(n!...)]))
>>> pred = define("pred", [(n, Pos)], Nat, n - 1)
>>> myid = define("myid", [(n, Nat)], Nat, pred(inc(n)))

Parameters:

• name (str)

• args (Telescope)

• T (SubSort)

• body (ExprRef)

Return type:

FuncDeclRef