The syntax `[a, b, c]`

is shorthand for `a :: b :: c :: []`

, or
`List.cons a (List.cons b (List.cons c List.nil))`

. It allows conveniently constructing
list literals.

For lists of length at least 64, an alternative desugaring strategy is used
which uses let bindings as intermediates as in
`let left := [d, e, f]; a :: b :: c :: left`

to avoid creating very deep expressions.
Note that this changes the order of evaluation, although it should not be observable
unless you use side effecting operations like `dbg_trace`

.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Auxiliary syntax for implementing `[$elem,*]`

list literal syntax.
The syntax `%[a,b,c|tail]`

constructs a value equivalent to `a::b::c::tail`

.
It uses binary partitioning to construct a tree of intermediate let bindings as in
`let left := [d, e, f]; a :: b :: c :: left`

to avoid creating very deep expressions.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Auxiliary for `List.reverse`

. `List.reverseAux l r = l.reverse ++ r`

, but it is defined directly.

## Equations

- List.reverseAux [] x = x
- List.reverseAux (a :: l) x = List.reverseAux l (a :: x)

## Instances For

`O(|as|)`

. Reverse of a list:

`[1, 2, 3, 4].reverse = [4, 3, 2, 1]`

Note that because of the "functional but in place" optimization implemented by Lean's compiler, this function works without any allocations provided that the input list is unshared: it simply walks the linked list and reverses all the node pointers.

## Equations

- List.reverse as = List.reverseAux as []

## Instances For

`O(|xs|)`

: append two lists. `[1, 2, 3] ++ [4, 5] = [1, 2, 3, 4, 5]`

.
It takes time proportional to the first list.

## Equations

- List.append [] x = x
- List.append (a :: l) x = a :: List.append l x

## Instances For

Tail-recursive version of `List.append`

.

## Equations

- List.appendTR as bs = List.reverseAux (List.reverse as) bs

## Instances For

## Equations

- List.instEmptyCollectionList = { emptyCollection := [] }

`O(|l|)`

. `erase l a`

removes the first occurrence of `a`

from `l`

.

## Equations

- List.erase [] x = []
- List.erase (a :: as) x = match a == x with | true => as | false => a :: List.erase as x

## Instances For

`O(i)`

. `eraseIdx l i`

removes the `i`

'th element of the list `l`

.

`erase [a, b, c, d, e] 0 = [b, c, d, e]`

`erase [a, b, c, d, e] 1 = [a, c, d, e]`

`erase [a, b, c, d, e] 5 = [a, b, c, d, e]`

## Equations

- List.eraseIdx [] x = []
- List.eraseIdx (head :: as) 0 = as
- List.eraseIdx (a :: as) (Nat.succ n) = a :: List.eraseIdx as n

## Instances For

Tail-recursive version of `List.map`

.

## Equations

- List.mapTR f as = List.mapTR.loop f as []

## Instances For

## Equations

- List.mapTR.loop f [] x = List.reverse x
- List.mapTR.loop f (a :: as) x = List.mapTR.loop f as (f a :: x)

## Instances For

`O(|l|)`

. `filterMap f l`

takes a function `f : α → Option β`

and applies it to each element of `l`

;
the resulting non-`none`

values are collected to form the output list.

```
filterMap
(fun x => if x > 2 then some (2 * x) else none)
[1, 2, 5, 2, 7, 7]
= [10, 14, 14]
```

## Equations

- List.filterMap f [] = []
- List.filterMap f (head :: tail) = match f head with | none => List.filterMap f tail | some b => b :: List.filterMap f tail

## Instances For

`O(|l|)`

. `filter f l`

returns the list of elements in `l`

for which `f`

returns true.

```
filter (· > 2) [1, 2, 5, 2, 7, 7] = [5, 7, 7]
```

## Equations

- List.filter p [] = []
- List.filter p (head :: tail) = match p head with | true => head :: List.filter p tail | false => List.filter p tail

## Instances For

Tail-recursive version of `List.filter`

.

## Equations

- List.filterTR p as = List.filterTR.loop p as []

## Instances For

## Equations

- List.filterTR.loop p [] x = List.reverse x
- List.filterTR.loop p (a :: l) x = match p a with | true => List.filterTR.loop p l (a :: x) | false => List.filterTR.loop p l x

## Instances For

`O(|l|)`

. `partition p l`

calls `p`

on each element of `l`

, partitioning the list into two lists
`(l_true, l_false)`

where `l_true`

has the elements where `p`

was true
and `l_false`

has the elements where `p`

is false.
`partition p l = (filter p l, filter (not ∘ p) l)`

, but it is slightly more efficient
since it only has to do one pass over the list.

```
partition (· > 2) [1, 2, 5, 2, 7, 7] = ([5, 7, 7], [1, 2, 2])
```

## Equations

- List.partition p as = List.partition.loop p as ([], [])

## Instances For

## Equations

- List.partition.loop p [] (bs, cs) = (List.reverse bs, List.reverse cs)
- List.partition.loop p (a :: as) (bs, cs) = match p a with | true => List.partition.loop p as (a :: bs, cs) | false => List.partition.loop p as (bs, a :: cs)

## Instances For

`O(|l|)`

. `dropWhile p l`

removes elements from the list until it finds the first element
for which `p`

returns false; this element and everything after it is returned.

```
dropWhile (· < 4) [1, 3, 2, 4, 2, 7, 4] = [4, 2, 7, 4]
```

## Equations

- List.dropWhile p [] = []
- List.dropWhile p (head :: tail) = match p head with | true => List.dropWhile p tail | false => head :: tail

## Instances For

`O(|l|)`

. `find? p l`

returns the first element for which `p`

returns true,
or `none`

if no such element is found.

## Equations

- List.find? p [] = none
- List.find? p (head :: tail) = match p head with | true => some head | false => List.find? p tail

## Instances For

`O(|l|)`

. `findSome? f l`

applies `f`

to each element of `l`

, and returns the first non-`none`

result.

`findSome? (fun x => if x < 5 then some (10 * x) else none) [7, 6, 5, 8, 1, 2, 6] = some 10`

## Equations

- List.findSome? f [] = none
- List.findSome? f (head :: tail) = match f head with | some b => some b | none => List.findSome? f tail

## Instances For

`O(|l|)`

. `replace l a b`

replaces the first element in the list equal to `a`

with `b`

.

`replace [1, 4, 2, 3, 3, 7] 3 6 = [1, 4, 2, 6, 3, 7]`

`replace [1, 4, 2, 3, 3, 7] 5 6 = [1, 4, 2, 3, 3, 7]`

## Equations

- List.replace [] x✝ x = []
- List.replace (a :: as) x✝ x = match a == x✝ with | true => x :: as | false => a :: List.replace as x✝ x

## Instances For

`O(|l|)`

. `elem a l`

or `l.contains a`

is true if there is an element in `l`

equal to `a`

.

## Equations

- List.contains as a = List.elem a as

## Instances For

`a ∈ l`

is a predicate which asserts that `a`

is in the list `l`

.
Unlike `elem`

, this uses `=`

instead of `==`

and is suited for mathematical reasoning.

`a ∈ [x, y, z] ↔ a = x ∨ a = y ∨ a = z`

- head: ∀ {α : Type u} {a : α} (as : List α), List.Mem a (a :: as)
The head of a list is a member:

`a ∈ a :: as`

. - tail: ∀ {α : Type u} {a : α} (b : α) {as : List α}, List.Mem a as → List.Mem a (b :: as)
A member of the tail of a list is a member of the list:

`a ∈ l → a ∈ b :: l`

.

## Instances For

## Equations

- List.instMembershipList = { mem := List.Mem }

`O(|l|^2)`

. Erase duplicated elements in the list.
Keeps the first occurrence of duplicated elements.

`eraseDups [1, 3, 2, 2, 3, 5] = [1, 3, 2, 5]`

## Equations

- List.eraseDups as = List.eraseDups.loop as []

## Instances For

## Equations

- List.eraseDups.loop [] x = List.reverse x
- List.eraseDups.loop (a :: l) x = match List.elem a x with | true => List.eraseDups.loop l x | false => List.eraseDups.loop l (a :: x)

## Instances For

`O(|l|)`

. Erase repeated adjacent elements. Keeps the first occurrence of each run.

`eraseReps [1, 3, 2, 2, 2, 3, 5] = [1, 3, 2, 3, 5]`

## Equations

- List.eraseReps x = match x with | [] => [] | a :: as => List.eraseReps.loop a as []

## Instances For

## Equations

- List.eraseReps.loop x✝ [] x = List.reverse (x✝ :: x)
- List.eraseReps.loop x✝ (a' :: as) x = match x✝ == a' with | true => List.eraseReps.loop x✝ as x | false => List.eraseReps.loop a' as (x✝ :: x)

## Instances For

`O(|l|)`

. `span p l`

splits the list `l`

into two parts, where the first part
contains the longest initial segment for which `p`

returns true
and the second part is everything else.

`span (· > 5) [6, 8, 9, 5, 2, 9] = ([6, 8, 9], [5, 2, 9])`

`span (· > 10) [6, 8, 9, 5, 2, 9] = ([6, 8, 9, 5, 2, 9], [])`

## Equations

- List.span p as = List.span.loop p as []

## Instances For

## Equations

- List.span.loop p [] x = (List.reverse x, [])
- List.span.loop p (a :: l) x = match p a with | true => List.span.loop p l (a :: x) | false => (List.reverse x, a :: l)

## Instances For

`O(|l|)`

. `groupBy R l`

splits `l`

into chains of elements
such that adjacent elements are related by `R`

.

`groupBy (·==·) [1, 1, 2, 2, 2, 3, 2] = [[1, 1], [2, 2, 2], [3], [2]]`

`groupBy (·<·) [1, 2, 5, 4, 5, 1, 4] = [[1, 2, 5], [4, 5], [1, 4]]`

## Equations

- List.groupBy R x = match x with | [] => [] | a :: as => List.groupBy.loop R as a [] []

## Instances For

## Equations

- List.groupBy.loop R (a :: as) x✝¹ x✝ x = match R x✝¹ a with | true => List.groupBy.loop R as a (x✝¹ :: x✝) x | false => List.groupBy.loop R as a [] (List.reverse (x✝¹ :: x✝) :: x)
- List.groupBy.loop R [] x✝¹ x✝ x = List.reverse (List.reverse (x✝¹ :: x✝) :: x)

## Instances For

`O(|l|)`

. `lookup a l`

treats `l : List (α × β)`

like an association list,
and returns the first `β`

value corresponding to an `α`

value in the list equal to `a`

.

## Equations

- List.lookup x [] = none
- List.lookup x ((k, b) :: es) = match x == k with | true => some b | false => List.lookup x es

## Instances For

`O(|xs|)`

. Computes the "set difference" of lists,
by filtering out all elements of `xs`

which are also in `ys`

.

`removeAll [1, 1, 5, 1, 2, 4, 5] [1, 2, 2] = [5, 4, 5]`

## Equations

- List.removeAll xs ys = List.filter (fun (x : α) => List.notElem x ys) xs

## Instances For

`O(|xs|)`

. Returns the longest initial segment of `xs`

for which `p`

returns true.

## Equations

- List.takeWhile p [] = []
- List.takeWhile p (head :: tail) = match p head with | true => head :: List.takeWhile p tail | false => []

## Instances For

`O(|l|)`

. Applies function `f`

to all of the elements of the list, from right to left.

`foldr f init [a, b, c] = f a <| f b <| f c <| init`

## Equations

- List.foldr f init [] = init
- List.foldr f init (head :: tail) = f head (List.foldr f init tail)

## Instances For

`O(min |xs| |ys|)`

. Applies `f`

to the two lists in parallel, stopping at the shorter list.

`zipWith f [x₁, x₂, x₃] [y₁, y₂, y₃, y₄] = [f x₁ y₁, f x₂ y₂, f x₃ y₃]`

## Equations

- List.zipWith f (x_2 :: xs) (y :: ys) = f x_2 y :: List.zipWith f xs ys
- List.zipWith f x✝ x = []

## Instances For

`O(min |xs| |ys|)`

. Combines the two lists into a list of pairs, with one element from each list.
The longer list is truncated to match the shorter list.

`zip [x₁, x₂, x₃] [y₁, y₂, y₃, y₄] = [(x₁, y₁), (x₂, y₂), (x₃, y₃)]`

## Equations

- List.zip = List.zipWith Prod.mk

## Instances For

`O(max |xs| |ys|)`

.
Version of `List.zipWith`

that continues to the end of both lists,
passing `none`

to one argument once the shorter list has run out.

## Equations

- List.zipWithAll f [] x = List.map (fun (b : β) => f none (some b)) x
- List.zipWithAll f (a :: as) [] = List.map (fun (a : α) => f (some a) none) (a :: as)
- List.zipWithAll f (a :: as) (b :: bs) = f (some a) (some b) :: List.zipWithAll f as bs

## Instances For

`O(|l|)`

. Separates a list of pairs into two lists containing the first components and second components.

`unzip [(x₁, y₁), (x₂, y₂), (x₃, y₃)] = ([x₁, x₂, x₃], [y₁, y₂, y₃])`

## Equations

- List.unzip [] = ([], [])
- List.unzip ((a, b) :: t) = match List.unzip t with | (al, bl) => (a :: al, b :: bl)

## Instances For

`O(n)`

. `range n`

is the numbers from `0`

to `n`

exclusive, in increasing order.

`range 5 = [0, 1, 2, 3, 4]`

## Equations

- List.range n = List.range.loop n []

## Instances For

## Equations

- List.range.loop 0 x = x
- List.range.loop (Nat.succ n) x = List.range.loop n (n :: x)

## Instances For

## Equations

- List.iotaTR.go 0 x = List.reverse x
- List.iotaTR.go (Nat.succ n) x = List.iotaTR.go n (Nat.succ n :: x)

## Instances For

`O(|l|)`

. `enumFrom n l`

is like `enum`

but it allows you to specify the initial index.

`enumFrom 5 [a, b, c] = [(5, a), (6, b), (7, c)]`

## Equations

- List.enumFrom x [] = []
- List.enumFrom x (x_2 :: xs) = (x, x_2) :: List.enumFrom (x + 1) xs

## Instances For

`O(|l|)`

. `intersperse sep l`

alternates `sep`

and the elements of `l`

:

`intersperse sep [] = []`

`intersperse sep [a] = [a]`

`intersperse sep [a, b] = [a, sep, b]`

`intersperse sep [a, b, c] = [a, sep, b, sep, c]`

## Equations

- List.intersperse sep [] = []
- List.intersperse sep [x_1] = [x_1]
- List.intersperse sep (x_1 :: xs) = x_1 :: sep :: List.intersperse sep xs

## Instances For

`O(|xs|)`

. `intercalate sep xs`

alternates `sep`

and the elements of `xs`

:

`intercalate sep [] = []`

`intercalate sep [a] = a`

`intercalate sep [a, b] = a ++ sep ++ b`

`intercalate sep [a, b, c] = a ++ sep ++ b ++ sep ++ c`

## Equations

- List.intercalate sep xs = List.join (List.intersperse sep xs)

## Instances For

`bind xs f`

is the bind operation of the list monad. It applies `f`

to each element of `xs`

to get a list of lists, and then concatenates them all together.

## Instances For

The lexicographic order on lists.
`[] < a::as`

, and `a::as < b::bs`

if `a < b`

or if `a`

and `b`

are equivalent and `as < bs`

.

- nil: ∀ {α : Type u} [inst : LT α] (b : α) (bs : List α), List.lt [] (b :: bs)
`[]`

is the smallest element in the order. - head: ∀ {α : Type u} [inst : LT α] {a : α} (as : List α) {b : α} (bs : List α), a < b → List.lt (a :: as) (b :: bs)
If

`a < b`

then`a::as < b::bs`

. - tail: ∀ {α : Type u} [inst : LT α] {a : α} {as : List α} {b : α} {bs : List α},
¬a < b → ¬b < a → List.lt as bs → List.lt (a :: as) (b :: bs)
If

`a`

and`b`

are equivalent and`as < bs`

, then`a::as < b::bs`

.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.
- List.hasDecidableLt [] [] = isFalse ⋯
- List.hasDecidableLt [] (head :: tail) = isTrue ⋯
- List.hasDecidableLt (head :: tail) [] = isFalse ⋯

## Equations

`isPrefixOf l₁ l₂`

returns `true`

Iff `l₁`

is a prefix of `l₂`

.
That is, there exists a `t`

such that `l₂ == l₁ ++ t`

.

## Equations

- List.isPrefixOf [] x = true
- List.isPrefixOf x [] = false
- List.isPrefixOf (a :: as) (b :: bs) = (a == b && List.isPrefixOf as bs)

## Instances For

`isPrefixOf? l₁ l₂`

returns `some t`

when `l₂ == l₁ ++ t`

.

## Equations

- List.isPrefixOf? [] x = some x
- List.isPrefixOf? x [] = none
- List.isPrefixOf? (a :: as) (b :: bs) = if (a == b) = true then List.isPrefixOf? as bs else none

## Instances For

`isSuffixOf l₁ l₂`

returns `true`

Iff `l₁`

is a suffix of `l₂`

.
That is, there exists a `t`

such that `l₂ == t ++ l₁`

.

## Equations

- List.isSuffixOf l₁ l₂ = List.isPrefixOf (List.reverse l₁) (List.reverse l₂)

## Instances For

`isSuffixOf? l₁ l₂`

returns `some t`

when `l₂ == t ++ l₁`

.

## Equations

- List.isSuffixOf? l₁ l₂ = Option.map List.reverse (List.isPrefixOf? (List.reverse l₁) (List.reverse l₂))

## Instances For

`O(min |as| |bs|)`

. Returns true if `as`

and `bs`

have the same length,
and they are pairwise related by `eqv`

.

## Equations

- List.isEqv [] [] x = true
- List.isEqv (a :: as) (b :: bs) x = (x a b && List.isEqv as bs x)
- List.isEqv x✝¹ x✝ x = false

## Instances For

`replicate n a`

is `n`

copies of `a`

:

`replicate 5 a = [a, a, a, a, a]`

## Equations

- List.replicate 0 x = []
- List.replicate (Nat.succ n) x = x :: List.replicate n x

## Instances For

Tail-recursive version of `List.replicate`

.

## Equations

- List.replicateTR n a = List.replicateTR.loop a n []

## Instances For

## Equations

- List.replicateTR.loop a 0 x = x
- List.replicateTR.loop a (Nat.succ n) x = List.replicateTR.loop a n (a :: x)

## Instances For

Removes the last element of the list.

## Equations

- List.dropLast [] = []
- List.dropLast [x_1] = []
- List.dropLast (x_1 :: xs) = x_1 :: List.dropLast xs

## Instances For

Returns the largest element of the list, if it is not empty.

## Equations

- List.maximum? x = match x with | [] => none | a :: as => some (List.foldl max a as)

## Instances For

Returns the smallest element of the list, if it is not empty.

## Equations

- List.minimum? x = match x with | [] => none | a :: as => some (List.foldl min a as)

## Instances For

## Equations

- List.decidableBEx p [] = isFalse ⋯
- List.decidableBEx p (head :: tail) = if h₁ : p head then isTrue ⋯ else match List.decidableBEx p tail with | isTrue h₂ => isTrue ⋯ | isFalse h₂ => isFalse ⋯

## Equations

- List.decidableBAll p [] = isTrue ⋯
- List.decidableBAll p (head :: tail) = if h₁ : p head then match List.decidableBAll p tail with | isTrue h₂ => isTrue ⋯ | isFalse h₂ => isFalse ⋯ else isFalse ⋯