kdrag.datatype.define_primrec

kdrag.datatype.define_primrec(fun_name, vs: list[ExprRef], res_type: SortRef, **cases)

Define a function by primitive recursion. https://en.wikipedia.org/wiki/Primitive_recursive_function This is the analog of a fold.

>>> import kdrag.theories.nat as nat
>>> n, m = smt.Consts("n m", nat.Nat)
>>> myadd2 = define_primrec("myadd2", [n, m], nat.Nat,                                 Z = lambda: m,                                S = lambda a: nat.S(a))
>>> myadd2.defn
|= ForAll([n, m],
    myadd2(n, m) == If(is(S, n), S(myadd2(pred(n), m)), m))

Parameters:

• vs (list[ExprRef])

• res_type (SortRef)