Skip to content

List

Common operations for working with lists.

Return the first element of the list wrapped in Some, or None if the list is empty.

head : List<a> -> Option<a>head : List<a> -> Option<a>

tail

Return the list without its first element, or None if the list is empty.

tail : List<a> -> Option<List<a>>tail : List<a> -> Option<List<a>>

uncons

Return a pair (head, tail) wrapped in Some, or None if the list is empty.

uncons : List<a> -> Option<(a, List<a>)>uncons : List<a> -> Option<(a, List<a>)>

length

Return the length of the list as a natural number.

length : List<a> -> natlength : List<a> -> nat

reduce

Right-associative fold.

Apply the function to each element and an accumulator, starting from the end of the list.

reduce : (a -> b -> b) -> b -> List<a> -> breduce : (a -> b -> b) -> b -> List<a> -> b

reduce_left

Left-associative fold.

reduce_left : (b -> a -> b) -> b -> List<a> -> breduce_left : (b -> a -> b) -> b -> List<a> -> b

singleton

Return a list containing exactly one element.

singleton : a -> List<a>singleton : a -> List<a>

is_empty

Return true if the list is empty, or false otherwise.

is_empty : List<a> -> boolis_empty : List<a> -> bool

is_nonempty

Return true if the list contains any elements, or false otherwise.

is_nonempty : List<a> -> boolis_nonempty : List<a> -> bool

is_singleton

Return true if the list contains precisely one element, or false otherwise.

is_singleton : List<a> -> boolis_singleton : List<a> -> bool

concat

Flatten a list of lists into a single list.

concat : List<List<a>> -> List<a>concat : List<List<a>> -> List<a>

take

Return the first n elements of the list.

If the list is shorter than n, return the whole list.

take : nat -> List<a> -> List<a>take : nat -> List<a> -> List<a>

drop

Remove the first n elements from the list.

If the list is shorter than n, return an empty list.

drop : nat -> List<a> -> List<a>drop : nat -> List<a> -> List<a>

slice

Extract a range of elements from the list.

slice(m, n, xs) = xs |. drop(m) |. take(n - m)

slice : nat -> nat -> List<a> -> List<a>slice : nat -> nat -> List<a> -> List<a>

element_at

Return the element at index n, or None if out of bounds.

element_at : nat -> List<a> -> Option<a>element_at : nat -> List<a> -> Option<a>

map

Transform each element of a list using the given function.

map : (a -> b) -> List<a> -> List<b>map : (a -> b) -> List<a> -> List<b>

concat_map

Apply a function to every element of a list, where that function must return a list, and then concatenate the resulting lists into a single, flattened list.

concat_map : (a -> List<b>) -> List<a> -> List<b>concat_map : (a -> List<b>) -> List<a> -> List<b>

filter

Keep only the elements for which the predicate returns true.

filter : (a -> bool) -> List<a> -> List<a>filter : (a -> bool) -> List<a> -> List<a>

reverse

Return a new list with the elements in reverse order.

reverse : List<a> -> List<a>reverse : List<a> -> List<a>

unzip

Convert a list of pairs into a pair of lists, in the natural way.

E.g., unzip([(1, "one"), (2, "two")]) returns: ([1, 2], ["one", "two"])

unzip : List<(a, b)> -> (List<a>, List<b>)unzip : List<(a, b)> -> (List<a>, List<b>)

zip

Convert two lists into a list of pairs, in the natural way.

E.g., zip([1, 2], ["one", "two"]) returns: [(1, "one"), (2, "two")]

zip : List<a> -> List<b> -> List<(a, b)>zip : List<a> -> List<b> -> List<(a, b)>

any

Return true if and only if any element of the list satisfies the given predicate.

any : (a -> bool) -> List<a> -> boolany : (a -> bool) -> List<a> -> bool

all

Return true if and only if all element of the list satisfy the given predicate.

all : (a -> bool) -> List<a> -> boolall : (a -> bool) -> List<a> -> bool

all_true

Return the conjunction of a list of booleans.

all_true : List<bool> -> boolall_true : List<bool> -> bool

any_true

Return the disjunction of a list of booleans.

any_true : List<bool> -> boolany_true : List<bool> -> bool

find

Return the first element of the list that satisfies the given predicate, or None, if there is no such element.

find : (a -> bool) -> List<a> -> Option<a>find : (a -> bool) -> List<a> -> Option<a>

is_prefix_of

Return a boolean indicating whether the first list is a prefix of the second.

is_prefix_of : List<a> -> List<a> -> boolis_prefix_of : List<a> -> List<a> -> bool

range

Return the list [start, start + 1, ..., start + count - 1].

range : n -> nat -> List<n>range : n -> nat -> List<n>