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))
Select(Int.trans(Lambda(x, x + 1)), 2, 3)