kdrag.theories.list

Algebraic datatype of lists.

You may prefer using theories.seq which offers more builtin support for things like associativity.

Classes

List(Elt)

class kdrag.theories.list.List(Elt: SortRef)

Bases: object

Parameters:

Elt (SortRef)

of_list(xs: list[ExprRef]) → DatatypeRef

Helper to construct List values >>> IntList = List(smt.IntSort()) >>> IntList.of_list([1, 2, 3]) Cons(1, Cons(2, Cons(3, Nil)))

Parameters:

xs (list[ExprRef])

Return type:

DatatypeRef