kdrag.notation.trans_factory

kdrag.notation.trans_factory(Tstep: ArraySortRef) → FuncDeclRef

Transitive closure

>>> x = smt.Int("x")
>>> trans(smt.Lambda([x], x + 1), smt.IntVal(2), smt.IntVal(3))
Int.trans(Lambda(x, x + 1), 2, 3)