kdrag.theories.list

Algebraic datatype of lists.

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

Functions

`Cons`(x, xs)	Helper to construct Cons values >>> Cons(1, Nil(smt.IntSort())) Cons(1, Nil)
`List`(sort)	Build List sort >>> IntList = List(smt.IntSort()) >>> IntList.Cons(1, IntList.Nil) Cons(1, Nil)
`Nil`(sort)	Helper to construct Nil values >>> Nil(smt.IntSort()) Nil
`Unit`(x)	Helper to create Unit values >>> Unit(42) Cons(42, Nil) >>> Unit(42).sort() List_Int
`list`(*args)	Helper to construct List values >>> list(1, 2, 3) Cons(1, Cons(2, Cons(3, Nil)))

kdrag.theories.list.Cons(x: ExprRef, xs: DatatypeRef) → DatatypeRef

Helper to construct Cons values >>> Cons(1, Nil(smt.IntSort())) Cons(1, Nil)

Parameters:

Return type:

DatatypeRef

kdrag.theories.list.List(sort: SortRef) → DatatypeSortRef

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

kdrag.theories.list.Nil(sort: SortRef) → DatatypeRef

Helper to construct Nil values >>> Nil(smt.IntSort()) Nil

kdrag.theories.list.Unit(x: ExprRef) → DatatypeRef

Helper to create Unit values >>> Unit(42) Cons(42, Nil) >>> Unit(42).sort() List_Int

kdrag.theories.list.list(*args: ExprRef) → DatatypeRef

Helper to construct List values >>> list(1, 2, 3) Cons(1, Cons(2, Cons(3, Nil)))