Length of a list.

>>> sat $ \(l :: SList Word16) -> length l .== 2
Satisfiable. Model:
  s0 = [0,0] :: [Word16]
>>> sat $ \(l :: SList Word16) -> length l .< 0
Unsatisfiable
>>> prove $ \(l1 :: SList Word16) (l2 :: SList Word16) -> length l1 + length l2 .== length (l1 .++ l2)
Q.E.D.

null s is True iff the list is empty

>>> prove $ \(l :: SList Word16) -> null l .<=> length l .== 0
Q.E.D.
>>> prove $ \(l :: SList Word16) -> null l .<=> l .== []
Q.E.D.

head returns the first element of a list. Unspecified if the list is empty.

>>> prove $ \c -> head (singleton c) .== (c :: SInteger)
Q.E.D.

tail returns the tail of a list. Unspecified if the list is empty.

>>> prove $ \(h :: SInteger) t -> tail (singleton h .++ t) .== t
Q.E.D.
>>> prove $ \(l :: SList Integer) -> length l .> 0 .=> length (tail l) .== length l - 1
Q.E.D.
>>> prove $ \(l :: SList Integer) -> sNot (null l) .=> singleton (head l) .++ tail l .== l
Q.E.D.

uncons returns the pair of the head and tail. Unspecified if the list is empty.

init returns all but the last element of the list. Unspecified if the list is empty.

>>> prove $ \(h :: SInteger) t -> init (t .++ singleton h) .== t
Q.E.D.

singleton x is the list of length 1 that contains the only value x.

>>> prove $ \(x :: SInteger) -> head (singleton x) .== x
Q.E.D.
>>> prove $ \(x :: SInteger) -> length (singleton x) .== 1
Q.E.D.

listToListAt l offset. List of length 1 at offset in l. Unspecified if index is out of bounds.

>>> prove $ \(l1 :: SList Integer) l2 -> listToListAt (l1 .++ l2) (length l1) .== listToListAt l2 0
Q.E.D.
>>> sat $ \(l :: SList Word16) -> length l .>= 2 .&& listToListAt l 0 ./= listToListAt l (length l - 1)
Satisfiable. Model:
  s0 = [0,1] :: [Word16]

elemAt l i is the value stored at location i. Unspecified if index is out of bounds.

>>> prove $ \i -> i `inRange` (0, 4) .=> [1,1,1,1,1] `elemAt` i .== (1::SInteger)
Q.E.D.

• >>> prove $ (l :: SList Integer) i e -> i inRange (0, length l - 1) .&& l elemAt i .== e .=> indexOf l (singleton e) .<= i Q.E.D.

Short cut for elemAt

implode es is the list of length |es| containing precisely those elements. Note that there is no corresponding function explode, since we wouldn't know the length of a symbolic list.

>>> prove $ \(e1 :: SInteger) e2 e3 -> length (implode [e1, e2, e3]) .== 3
Q.E.D.
>>> prove $ \(e1 :: SInteger) e2 e3 -> map (elemAt (implode [e1, e2, e3])) (map literal [0 .. 2]) .== [e1, e2, e3]
Q.E.D.

Concatenate two lists. See also .++.

Prepend an element, the traditional cons.

Append an element

Empty list. This value has the property that it's the only list with length 0:

>>> prove $ \(l :: SList Integer) -> length l .== 0 .<=> l .== nil
Q.E.D.

Short cut for concat.

>>> sat $ \x y z -> length x .== 5 .&& length y .== 1 .&& x .++ y .++ z .== [1 .. 12]
Satisfiable. Model:
  s0 =      [1,2,3,4,5] :: [Integer]
  s1 =              [6] :: [Integer]
  s2 = [7,8,9,10,11,12] :: [Integer]

elem e l. Does l contain the element e?

notElem e l. Does l not contain the element e?

isInfixOf sub l. Does l contain the subsequence sub?

>>> prove $ \(l1 :: SList Integer) l2 l3 -> l2 `isInfixOf` (l1 .++ l2 .++ l3)
Q.E.D.
>>> prove $ \(l1 :: SList Integer) l2 -> l1 `isInfixOf` l2 .&& l2 `isInfixOf` l1 .<=> l1 .== l2
Q.E.D.

isSuffixOf suf l. Is suf a suffix of l?

>>> prove $ \(l1 :: SList Word16) l2 -> l2 `isSuffixOf` (l1 .++ l2)
Q.E.D.
>>> prove $ \(l1 :: SList Word16) l2 -> l1 `isSuffixOf` l2 .=> subList l2 (length l2 - length l1) (length l1) .== l1
Q.E.D.

isPrefixOf pre l. Is pre a prefix of l?

>>> prove $ \(l1 :: SList Integer) l2 -> l1 `isPrefixOf` (l1 .++ l2)
Q.E.D.
>>> prove $ \(l1 :: SList Integer) l2 -> l1 `isPrefixOf` l2 .=> subList l2 0 (length l1) .== l1
Q.E.D.

take len l. Corresponds to Haskell's take on symbolic lists.

>>> prove $ \(l :: SList Integer) i -> i .>= 0 .=> length (take i l) .<= i
Q.E.D.

drop len s. Corresponds to Haskell's drop on symbolic-lists.

>>> prove $ \(l :: SList Word16) i -> length (drop i l) .<= length l
Q.E.D.
>>> prove $ \(l :: SList Word16) i -> take i l .++ drop i l .== l
Q.E.D.

subList s offset len is the sublist of s at offset offset with length len. This function is under-specified when the offset is outside the range of positions in s or len is negative or offset+len exceeds the length of s.

>>> prove $ \(l :: SList Integer) i -> i .>= 0 .&& i .< length l .=> subList l 0 i .++ subList l i (length l - i) .== l
Q.E.D.
>>> sat  $ \i j -> subList [1..5] i j .== ([2..4] :: SList Integer)
Satisfiable. Model:
  s0 = 1 :: Integer
  s1 = 3 :: Integer
>>> sat  $ \i j -> subList [1..5] i j .== ([6..7] :: SList Integer)
Unsatisfiable

replace l src dst. Replace the first occurrence of src by dst in s

>>> prove $ \l -> replace [1..5] l [6..10] .== [6..10] .=> l .== ([1..5] :: SList Word8)
Q.E.D.
>>> prove $ \(l1 :: SList Integer) l2 l3 -> length l2 .> length l1 .=> replace l1 l2 l3 .== l1
Q.E.D.

indexOf l sub. Retrieves first position of sub in l, -1 if there are no occurrences. Equivalent to offsetIndexOf l sub 0.

• >>> prove $ (l :: SList Int8) i -> i .> 0 .&& i .l .= indexOf l (subList l i 1) .<= i Q.E.D.

>>> prove $ \(l1 :: SList Word16) l2 -> length l2 .> length l1 .=> indexOf l1 l2 .== -1
Q.E.D.

offsetIndexOf l sub offset. Retrieves first position of sub at or after offset in l, -1 if there are no occurrences.

>>> prove $ \(l :: SList Int8) sub -> offsetIndexOf l sub 0 .== indexOf l sub
Q.E.D.
>>> prove $ \(l :: SList Int8) sub i -> i .>= length l .&& length sub .> 0 .=> offsetIndexOf l sub i .== -1
Q.E.D.
>>> prove $ \(l :: SList Int8) sub i -> i .> length l .=> offsetIndexOf l sub i .== -1
Q.E.D.