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")
>>> inc = define("test_inc", [(n,Nat)], Pos, n + 1)
>>> inc.pre_post
|= ForAll(n!...,
       Implies(And(n!... >= 0), test_inc(n!...) > 0))
>>> pred = define("pred", [(n, Pos)], Nat, n - 1)
>>> myid = define("myid", [(n, Nat)], Nat, pred(inc(n)))
Parameters:
Return type:

FuncDeclRef