kdrag.datatype.define_fun

kdrag.datatype.define_fun(eqs)

Define a function by pattern matching equations.

>>> import kdrag.theories.nat as nat
>>> n, m = smt.Consts("n m", nat.Nat)
>>> myadd = smt.Function("myadd", nat.Nat, nat.Nat, nat.Nat)
>>> myadd = define_fun([myadd(nat.Z, m)    == m,                            myadd(nat.S(n), m) == nat.S(myadd(n, m))])
>>> myadd.case0
|- ForAll(m, myadd(Z, m) == m)
>>> myadd.case1
|- ForAll([n, m], myadd(S(n), m) == S(myadd(n, m)))