kdrag.theories.list

Algebraic datatype of lists.

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

Functions

List(Elt)

Classes

List_(Elt)

kdrag.theories.list.List(Elt: SortRef) → List_

>>> IntList = List(smt.IntSort())
>>> IntList.Cons(1, IntList.Nil)
Cons(1, Nil)

Parameters:

Elt (SortRef)

Return type:

List_

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