kdrag.theories.seq.Seq

kdrag.theories.seq.Seq(T: SortRef) → SeqSortRef

Make sort of Sequences and prove useful lemmas.

>>> BoolSeq = Seq(smt.BoolSort())
>>> x,y,z = smt.Consts("x y z", BoolSeq)
>>> x + y
Concat(x, y)