kdrag.theories.list

Algebraic datatype of lists.

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

Functions

ListSort(Elt)

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

kdrag.theories.list.ListSort(Elt: SortRef) → DatatypeSortRef

>>> ListSort(smt.IntSort())
List_Int...

Parameters:

Elt (SortRef)

Return type:

DatatypeSortRef