list.split_at

Split a list at an index.

split_at 2 [a, b, c] = ([a, b], [c])

list.split_on_p

Split a list at every element satisfying a predicate.

list.split_on

Split a list at every occurrence of an element.

[1,1,2,3,2,4,4].split_on 2 = [[1,1],[3],[4,4]]

list.concat

Concatenate an element at the end of a list.

concat [a, b] c = [a, b, c]

list.to_array

Convert a list into an array (whose length is the length of l).

list.inth

"inhabited" nth function: returns default instead of none in the case that the index is out of bounds.

list.modify_nth_tail

Apply a function to the nth tail of l. Returns the input without using f if the index is larger than the length of the list.

modify_nth_tail f 2 [a, b, c] = [a, b] ++ f [c]

list.modify_head

Apply f to the head of the list, if it exists.

list.modify_nth

Apply f to the nth element of the list, if it exists.

list.take_while

Get the longest initial segment of the list whose members all satisfy p.

take_while (λ x, x < 3) [0, 2, 5, 1] = [0, 2]

list.scanl

Fold a function f over the list from the left, returning the list of partial results.

scanl (+) 0 [1, 2, 3] = [0, 1, 3, 6]

list.scanr

Fold a function f over the list from the right, returning the list of partial results.

scanr (+) 0 [1, 2, 3] = [6, 5, 3, 0]

list.prod

Product of a list.

prod [a, b, c] = ((1 * a) * b) * c

list.sum

Sum of a list.

sum [a, b, c] = ((0 + a) + b) + c

list.find

find p l is the first element of l satisfying p, or none if no such element exists.

list.find_indexes

find_indexes p l is the list of indexes of elements of l that satisfy p.

list.lookmap

lookmap is a combination of lookup and filter_map. lookmap f l will apply f : α → option α to each element of the list, replacing a → b at the first value a in the list such that f a = some b.

list.indexes_of

indexes_of a l is the list of all indexes of a in l.

indexes_of a [a, b, a, a] = [0, 2, 3]

list.countp

countp p l is the number of elements of l that satisfy p.

list.count

count a l is the number of occurrences of a in l.

list.is_prefix

is_prefix l₁ l₂, or l₁ <+: l₂, means that l₁ is a prefix of l₂, that is, l₂ has the form l₁ ++ t for some t.

list.is_suffix

is_suffix l₁ l₂, or l₁ <:+ l₂, means that l₁ is a suffix of l₂, that is, l₂ has the form t ++ l₁ for some t.

list.is_infix

is_infix l₁ l₂, or l₁ <:+: l₂, means that l₁ is a contiguous substring of l₂, that is, l₂ has the form s ++ l₁ ++ t for some s, t.

list.inits

inits l is the list of initial segments of l.

inits [1, 2, 3] = [[], [1], [1, 2], [1, 2, 3]]

list.tails

tails l is the list of terminal segments of l.

tails [1, 2, 3] = [[1, 2, 3], [2, 3], [3], []]

list.sublists'

sublists' l is the list of all (non-contiguous) sublists of l. It differs from sublists only in the order of appearance of the sublists; sublists' uses the first element of the list as the MSB, sublists uses the first element of the list as the LSB.

sublists' [1, 2, 3] = [[], [3], [2], [2, 3], [1], [1, 3], [1, 2], [1, 2, 3]]

list.sublists

sublists l is the list of all (non-contiguous) sublists of l; cf. sublists' for a different ordering.

sublists [1, 2, 3] = [[], [1], [2], [1, 2], [3], [1, 3], [2, 3], [1, 2, 3]]

list.transpose

transpose of a list of lists, treated as a matrix.

transpose [[1, 2], [3, 4], [5, 6]] = [[1, 3, 5], [2, 4, 6]]

list.sections

List of all sections through a list of lists. A section of [L₁, L₂, ..., Lₙ] is a list whose first element comes from L₁, whose second element comes from L₂, and so on.

list.permutations

List of all permutations of l.

permutations [1, 2, 3] =
  [[1, 2, 3], [2, 1, 3], [3, 2, 1],
   [2, 3, 1], [3, 1, 2], [1, 3, 2]]

list.product

product l₁ l₂ is the list of pairs (a, b) where a ∈ l₁ and b ∈ l₂.

product [1, 2] [5, 6] = [(1, 5), (1, 6), (2, 5), (2, 6)]

list.sigma

sigma l₁ l₂ is the list of dependent pairs (a, b) where a ∈ l₁ and b ∈ l₂ a.

sigma [1, 2] (λ_, [(5 : ℕ), 6]) = [(1, 5), (1, 6), (2, 5), (2, 6)]

list.disjoint

disjoint l₁ l₂ means that l₁ and l₂ have no elements in common.

list.pairwise

pairwise R l means that all the elements with earlier indexes are R-related to all the elements with later indexes.

pairwise R [1, 2, 3] ↔ R 1 2 ∧ R 1 3 ∧ R 2 3

For example if R = (≠) then it asserts l has no duplicates, and if R = (<) then it asserts that l is (strictly) sorted.

list.pw_filter

pw_filter R l is a maximal sublist of l which is pairwise R. pw_filter (≠) is the erase duplicates function (cf. erase_dup), and pw_filter (<) finds a maximal increasing subsequence in l. For example,

pw_filter (<) [0, 1, 5, 2, 6, 3, 4] = [0, 1, 2, 3, 4]

list.chain

chain R a l means that R holds between adjacent elements of a::l.

chain R a [b, c, d] ↔ R a b ∧ R b c ∧ R c d

list.chain'

chain' R l means that R holds between adjacent elements of l.

chain' R [a, b, c, d] ↔ R a b ∧ R b c ∧ R c d

list.nodup

nodup l means that l has no duplicates, that is, any element appears at most once in the list. It is defined as pairwise (≠).

list.erase_dup

erase_dup l removes duplicates from l (taking only the first occurrence). Defined as pw_filter (≠).

erase_dup [1, 0, 2, 2, 1] = [0, 2, 1]

list.range'

range' s n is the list of numbers [s, s+1, ..., s+n-1]. It is intended mainly for proving properties of range and iota.

list.ilast'

ilast' x xs returns the last element of xs if xs is non-empty; it returns x otherwise

list.last'

last' xs returns the last element of xs if xs is non-empty; it returns none otherwise

list.rotate

rotate l n rotates the elements of l to the left by n

rotate [0, 1, 2, 3, 4, 5] 2 = [2, 3, 4, 5, 0, 1]

list.rotate'

rotate' is the same as rotate, but slower. Used for proofs about rotate

list.mmap_filter

Filters and maps elements of a list

list.get_rest

get_rest l l₁ returns some l₂ if l = l₁ ++ l₂. If l₁ is not a prefix of l, returns none