# Basic operations on List. #

We define

• basic operations on List,
• simp lemmas for applying the operations on .nil and .cons arguments (in the cases where the right hand side is simple to state; otherwise these are deferred to Init.Data.List.Lemmas),
• the minimal lemmas which are required for setting up Init.Data.Array.Basic.

In Init.Data.List.Impl we give tail-recursive versions of these operations along with @[csimp] lemmas,

In Init.Data.List.Lemmas we develop the full API for these functions.

Recall that length, get, set, fold, and concat have already been defined in Init.Prelude.

The operations are organized as follow:

Further operations are defined in Init.Data.List.BasicAux (because they use Array in their implementations), namely:

## Preliminaries from Init.Prelude#

### length #

@[simp]
theorem List.length_nil {α : Type u} :
[].length = 0
@[simp]
theorem List.length_singleton {α : Type u} (a : α) :
[a].length = 1
@[simp]
theorem List.length_cons {α : Type u_1} (a : α) (as : List α) :
(a :: as).length = as.length + 1

### set #

@[simp]
theorem List.length_set {α : Type u} (as : List α) (i : Nat) (a : α) :
(as.set i a).length = as.length

### foldl #

@[simp]
theorem List.foldl_nil :
∀ {α : Type u_1} {β : Type u_2} {f : αβα} {b : α}, List.foldl f b [] = b
@[simp]
theorem List.foldl_cons {α : Type u} {β : Type v} {a : α} {f : βαβ} (l : List α) (b : β) :
List.foldl f b (a :: l) = List.foldl f (f b a) l

### concat #

@[simp]
theorem List.length_concat {α : Type u} (as : List α) (a : α) :
(as.concat a).length = as.length + 1
theorem List.of_concat_eq_concat {α : Type u} {as : List α} {bs : List α} {a : α} {b : α} (h : as.concat a = bs.concat b) :
as = bs a = b

## Equality #

def List.beq {α : Type u} [BEq α] :
List αList αBool

The equality relation on lists asserts that they have the same length and they are pairwise BEq.

Equations
Instances For
instance List.instBEq {α : Type u} [BEq α] :
BEq (List α)
Equations
• List.instBEq = { beq := List.beq }
instance List.instLawfulBEq {α : Type u} [BEq α] [] :
Equations
• =
@[specialize #[]]
def List.isEqv {α : Type u} (as : List α) (bs : List α) (eqv : ααBool) :

O(min |as| |bs|). Returns true if as and bs have the same length, and they are pairwise related by eqv.

Equations
• [].isEqv [] x = true
• (a :: as).isEqv (b :: bs) x = (x a b && as.isEqv bs x)
• x✝¹.isEqv x✝ x = false
Instances For
@[simp]
theorem List.isEqv_nil_nil {α : Type u} {eqv : ααBool} :
[].isEqv [] eqv = true
@[simp]
theorem List.isEqv_nil_cons {α : Type u} {a : α} {as : List α} {eqv : ααBool} :
[].isEqv (a :: as) eqv = false
@[simp]
theorem List.isEqv_cons_nil {α : Type u} {a : α} {as : List α} {eqv : ααBool} :
(a :: as).isEqv [] eqv = false
theorem List.isEqv_cons₂ :
∀ {α : Type u_1} {a : α} {as : List α} {b : α} {bs : List α} {eqv : ααBool}, (a :: as).isEqv (b :: bs) eqv = (eqv a b && as.isEqv bs eqv)

## Lexicographic ordering #

inductive List.lt {α : Type u} [LT α] :
List αList αProp

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 α), [].lt (b :: bs)

[] is the smallest element in the order.

• head: ∀ {α : Type u} [inst : LT α] {a : α} (as : List α) {b : α} (bs : List α), a < b(a :: as).lt (b :: bs)

If a < b then a::as < b::bs.

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

If a and b are equivalent and as < bs, then a::as < b::bs.

Instances For
instance List.instLT {α : Type u} [LT α] :
LT (List α)
Equations
• List.instLT = { lt := List.lt }
instance List.hasDecidableLt {α : Type u} [LT α] [h : DecidableRel fun (x x_1 : α) => x < x_1] (l₁ : List α) (l₂ : List α) :
Decidable (l₁ < l₂)
Equations
• One or more equations did not get rendered due to their size.
• [].hasDecidableLt [] =
• [].hasDecidableLt (head :: tail) =
• (head :: tail).hasDecidableLt [] =
@[reducible]
def List.le {α : Type u} [LT α] (a : List α) (b : List α) :

The lexicographic order on lists.

Equations
Instances For
instance List.instLEOfLT {α : Type u} [LT α] :
LE (List α)
Equations
• List.instLEOfLT = { le := List.le }
instance List.instDecidableLeOfDecidableRelLt {α : Type u} [LT α] [DecidableRel fun (x x_1 : α) => x < x_1] (l₁ : List α) (l₂ : List α) :
Decidable (l₁ l₂)
Equations

## Alternative getters #

### get? #

def List.get? {α : Type u} (as : List α) (i : Nat) :

Returns the i-th element in the list (zero-based).

If the index is out of bounds (i ≥ as.length), this function returns none. Also see get, getD and get!.

Equations
• (a :: tail).get? 0 = some a
• (head :: as).get? n.succ = as.get? n
• x✝.get? x = none
Instances For
@[simp]
theorem List.get?_nil {α : Type u} {n : Nat} :
[].get? n = none
@[simp]
theorem List.get?_cons_zero {α : Type u} {a : α} {l : List α} :
(a :: l).get? 0 = some a
@[simp]
theorem List.get?_cons_succ {α : Type u} {a : α} {l : List α} {n : Nat} :
(a :: l).get? (n + 1) = l.get? n
theorem List.ext_get? {α : Type u} {l₁ : List α} {l₂ : List α} :
(∀ (n : Nat), l₁.get? n = l₂.get? n)l₁ = l₂
@[reducible, inline, deprecated]
abbrev List.ext {α : Type u_1} {l₁ : List α} {l₂ : List α} :
(∀ (n : Nat), l₁.get? n = l₂.get? n)l₁ = l₂

Deprecated alias for ext_get?. The preferred extensionality theorem is now ext_getElem?.

Equations
Instances For

### getD #

def List.getD {α : Type u} (as : List α) (i : Nat) (fallback : α) :
α

Returns the i-th element in the list (zero-based).

If the index is out of bounds (i ≥ as.length), this function returns fallback. See also get? and get!.

Equations
• as.getD i fallback = (as.get? i).getD fallback
Instances For
@[simp]
theorem List.getD_nil {n : Nat} :
∀ {α : Type u_1} {d : α}, [].getD n d = d
@[simp]
theorem List.getD_cons_zero :
∀ {α : Type u_1} {x : α} {xs : List α} {d : α}, (x :: xs).getD 0 d = x
@[simp]
theorem List.getD_cons_succ :
∀ {α : Type u_1} {x : α} {xs : List α} {n : Nat} {d : α}, (x :: xs).getD (n + 1) d = xs.getD n d

### getLast #

def List.getLast {α : Type u} (as : List α) :
as []α

Returns the last element of a non-empty list.

Equations
• [].getLast h = absurd h
• [a].getLast x_2 = a
• (head :: b :: as).getLast x_2 = (b :: as).getLast
Instances For

### getLast? #

def List.getLast? {α : Type u} :
List α

Returns the last element in the list.

If the list is empty, this function returns none. Also see getLastD and getLast!.

Equations
• x.getLast? = match x with | [] => none | a :: as => some ((a :: as).getLast )
Instances For
@[simp]
theorem List.getLast?_nil {α : Type u} :
[].getLast? = none

### getLastD #

def List.getLastD {α : Type u} (as : List α) (fallback : α) :
α

Returns the last element in the list.

If the list is empty, this function returns fallback. Also see getLast? and getLast!.

Equations
• x✝.getLastD x = match x✝, x with | [], a₀ => a₀ | a :: as, x => (a :: as).getLast
Instances For
@[simp]
theorem List.getLastD_nil {α : Type u} (a : α) :
[].getLastD a = a
@[simp]
theorem List.getLastD_cons {α : Type u} (a : α) (b : α) (l : List α) :
(b :: l).getLastD a = l.getLastD b

def List.head {α : Type u} (as : List α) :
as []α

Returns the first element of a non-empty list.

Equations
• x✝.head x = match x✝, x with | a :: tail, x => a
Instances For
@[simp]
theorem List.head_cons {α : Type u} {a : α} {l : List α} {h : a :: l []} :
(a :: l).head h = a
def List.head? {α : Type u} :
List α

Returns the first element in the list.

If the list is empty, this function returns none. Also see headD and head!.

Equations
• x.head? = match x with | [] => none | a :: tail => some a
Instances For
@[simp]
theorem List.head?_nil {α : Type u} :
@[simp]
theorem List.head?_cons {α : Type u} {a : α} {l : List α} :
(a :: l).head? = some a

def List.headD {α : Type u} (as : List α) (fallback : α) :
α

Returns the first element in the list.

If the list is empty, this function returns fallback. Also see head? and head!.

Equations
• x✝.headD x = match x✝, x with | [], fallback => fallback | a :: tail, x => a
Instances For
@[simp]
theorem List.headD_nil {α : Type u} {d : α} :
@[simp]
theorem List.headD_cons {α : Type u} {a : α} {l : List α} {d : α} :
(a :: l).headD d = a

### tail? #

def List.tail? {α : Type u} :
List αOption (List α)

Drops the first element of the list.

If the list is empty, this function returns none. Also see tailD and tail!.

Equations
• x.tail? = match x with | [] => none | head :: as => some as
Instances For
@[simp]
theorem List.tail?_nil {α : Type u} :
[].tail? = none
@[simp]
theorem List.tail?_cons {α : Type u} {a : α} {l : List α} :
(a :: l).tail? = some l

### tailD #

def List.tailD {α : Type u} (list : List α) (fallback : List α) :
List α

Drops the first element of the list.

If the list is empty, this function returns fallback. Also see head? and head!.

Equations
• list.tailD fallback = match list with | [] => fallback | head :: tl => tl
Instances For
@[simp]
theorem List.tailD_nil {α : Type u} {l' : List α} :
[].tailD l' = l'
@[simp]
theorem List.tailD_cons {α : Type u} {a : α} {l : List α} {l' : List α} :
(a :: l).tailD l' = l

## Basic List operations. #

We define the basic functional programming operations on List: map, filter, filterMap, foldr, append, join, pure, bind, replicate, and reverse.

### map #

@[specialize #[]]
def List.map {α : Type u} {β : Type v} (f : αβ) :
List αList β

O(|l|). map f l applies f to each element of the list.

• map f [a, b, c] = [f a, f b, f c]
Equations
Instances For
@[simp]
theorem List.map_nil {α : Type u} {β : Type v} {f : αβ} :
List.map f [] = []
@[simp]
theorem List.map_cons {α : Type u} {β : Type v} (f : αβ) (a : α) (l : List α) :
List.map f (a :: l) = f a :: List.map f l

### filter #

def List.filter {α : Type u} (p : αBool) :
List αList α

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
Instances For
@[simp]
theorem List.filter_nil {α : Type u} (p : αBool) :
List.filter p [] = []

### filterMap #

@[specialize #[]]
def List.filterMap {α : Type u} {β : Type v} (f : α) :
List αList β

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
Instances For
@[simp]
theorem List.filterMap_nil {α : Type u} {β : Type v} (f : α) :
= []
theorem List.filterMap_cons {α : Type u} {β : Type v} (f : α) (a : α) (l : List α) :
List.filterMap f (a :: l) = match f a with | none => | some b => b ::

### foldr #

@[specialize #[]]
def List.foldr {α : Type u} {β : Type v} (f : αββ) (init : β) :
List αβ

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
Instances For
@[simp]
theorem List.foldr_nil :
∀ {α : Type u_1} {α_1 : Type u_2} {f : αα_1α_1} {b : α_1}, List.foldr f b [] = b
@[simp]
theorem List.foldr_cons {α : Type u} {a : α} :
∀ {α_1 : Type u_1} {f : αα_1α_1} {b : α_1} (l : List α), List.foldr f b (a :: l) = f a (List.foldr f b l)

### reverse #

def List.reverseAux {α : Type u} :
List αList αList α

Auxiliary for List.reverse. List.reverseAux l r = l.reverse ++ r, but it is defined directly.

Equations
• [].reverseAux x = x
• (a :: l).reverseAux x = l.reverseAux (a :: x)
Instances For
@[simp]
theorem List.reverseAux_nil :
∀ {α : Type u_1} {r : List α}, [].reverseAux r = r
@[simp]
theorem List.reverseAux_cons :
∀ {α : Type u_1} {a : α} {l r : List α}, (a :: l).reverseAux r = l.reverseAux (a :: r)
def List.reverse {α : Type u} (as : List α) :
List α

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
• as.reverse = as.reverseAux []
Instances For
@[simp]
theorem List.reverse_nil {α : Type u} :
[].reverse = []
theorem List.reverseAux_reverseAux {α : Type u} (as : List α) (bs : List α) (cs : List α) :
(as.reverseAux bs).reverseAux cs = bs.reverseAux ((as.reverseAux []).reverseAux cs)

### append #

def List.append {α : Type u} (xs : List α) (ys : List α) :
List α

O(|xs|): append two lists. [1, 2, 3] ++ [4, 5] = [1, 2, 3, 4, 5]. It takes time proportional to the first list.

Equations
• [].append x = x
• (a :: l).append x = a :: l.append x
Instances For
def List.appendTR {α : Type u} (as : List α) (bs : List α) :
List α

Tail-recursive version of List.append.

Most of the tail-recursive implementations are in Init.Data.List.Impl, but appendTR must be set up immediately, because otherwise Append (List α) instance below will not use it.

Equations
• as.appendTR bs = as.reverse.reverseAux bs
Instances For
@[csimp]
instance List.instAppend {α : Type u} :
Equations
• List.instAppend = { append := List.append }
@[simp]
theorem List.append_eq {α : Type u} (as : List α) (bs : List α) :
as.append bs = as ++ bs
@[simp]
theorem List.nil_append {α : Type u} (as : List α) :
[] ++ as = as
@[simp]
theorem List.cons_append {α : Type u} (a : α) (as : List α) (bs : List α) :
a :: as ++ bs = a :: (as ++ bs)
@[simp]
theorem List.append_nil {α : Type u} (as : List α) :
as ++ [] = as
instance List.instLawfulIdentityHAppendNil {α : Type u} :
Std.LawfulIdentity (fun (x x_1 : List α) => x ++ x_1) []
Equations
• =
@[simp]
theorem List.length_append {α : Type u} (as : List α) (bs : List α) :
(as ++ bs).length = as.length + bs.length
@[simp]
theorem List.append_assoc {α : Type u} (as : List α) (bs : List α) (cs : List α) :
as ++ bs ++ cs = as ++ (bs ++ cs)
instance List.instAssociativeHAppend {α : Type u} :
Std.Associative fun (x x_1 : List α) => x ++ x_1
Equations
• =
theorem List.append_cons {α : Type u} (as : List α) (b : α) (bs : List α) :
as ++ b :: bs = as ++ [b] ++ bs
@[simp]
theorem List.concat_eq_append {α : Type u} (as : List α) (a : α) :
as.concat a = as ++ [a]
theorem List.reverseAux_eq_append {α : Type u} (as : List α) (bs : List α) :
as.reverseAux bs = as.reverseAux [] ++ bs
@[simp]
theorem List.reverse_cons {α : Type u} (a : α) (as : List α) :
(a :: as).reverse = as.reverse ++ [a]

### join #

def List.join {α : Type u} :
List (List α)List α

O(|join L|). join L concatenates all the lists in L into one list.

• join [[a], [], [b, c], [d, e, f]] = [a, b, c, d, e, f]
Equations
• [].join = []
• (a :: as).join = a ++ as.join
Instances For
@[simp]
theorem List.join_nil {α : Type u} :
[].join = []
@[simp]
theorem List.join_cons :
∀ {α : Type u_1} {l : List α} {ls : List (List α)}, (l :: ls).join = l ++ ls.join

### pure #

@[inline]
def List.pure {α : Type u} (a : α) :
List α

pure x = [x] is the pure operation of the list monad.

Equations
• = [a]
Instances For

### bind #

@[inline]
def List.bind {α : Type u} {β : Type v} (a : List α) (b : αList β) :
List β

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.

• [2, 3, 2].bind range = [0, 1, 0, 1, 2, 0, 1]
Equations
Instances For
@[simp]
theorem List.bind_nil {α : Type u} {β : Type v} (f : αList β) :
[].bind f = []
@[simp]
theorem List.bind_cons {α : Type u} {β : Type v} (x : α) (xs : List α) (f : αList β) :
(x :: xs).bind f = f x ++ xs.bind f
@[reducible, inline, deprecated List.bind_nil]
abbrev List.nil_bind {α : Type u_1} {β : Type u_2} (f : αList β) :
[].bind f = []
Equations
Instances For
@[reducible, inline, deprecated List.bind_cons]
abbrev List.cons_bind {α : Type u_1} {β : Type u_2} (x : α) (xs : List α) (f : αList β) :
(x :: xs).bind f = f x ++ xs.bind f
Equations
Instances For

### replicate #

def List.replicate {α : Type u} (n : Nat) (a : α) :
List α

replicate n a is n copies of a:

Equations
Instances For
@[simp]
theorem List.replicate_zero :
∀ {α : Type u_1} {a : α}, = []
theorem List.replicate_succ {α : Type u} (a : α) (n : Nat) :
List.replicate (n + 1) a = a ::
@[simp]
theorem List.length_replicate {α : Type u} (n : Nat) (a : α) :
().length = n

## List membership #

• L.contains a : Bool determines, using a [BEq α] instance, whether L contains an element · == a.
• a ∈ L : Prop is the proposition (only decidable if α has decidable equality) that L contains an element · = a.

### EmptyCollection #

instance List.instEmptyCollection {α : Type u} :
Equations
• List.instEmptyCollection = { emptyCollection := [] }
@[simp]
theorem List.empty_eq {α : Type u} :
= []

### isEmpty #

def List.isEmpty {α : Type u} :
List αBool

O(1). isEmpty l is true if the list is empty.

Equations
• x.isEmpty = match x with | [] => true | head :: tail => false
Instances For
@[simp]
theorem List.isEmpty_nil {α : Type u} :
[].isEmpty = true
@[simp]
theorem List.isEmpty_cons {α : Type u} {x : α} {xs : List α} :
(x :: xs).isEmpty = false

### elem #

def List.elem {α : Type u} [BEq α] (a : α) :
List αBool

O(|l|). elem a l or l.contains a is true if there is an element in l equal to a.

• elem 3 [1, 4, 2, 3, 3, 7] = true
• elem 5 [1, 4, 2, 3, 3, 7] = false
Equations
Instances For
@[simp]
theorem List.elem_nil {α : Type u} {a : α} [BEq α] :
theorem List.elem_cons {α : Type u} {b : α} {bs : List α} [BEq α] {a : α} :
List.elem a (b :: bs) = match a == b with | true => true | false => List.elem a bs
@[deprecated]
def List.notElem {α : Type u} [BEq α] (a : α) (as : List α) :

notElem a l is !(elem a l).

Equations
Instances For

### contains #

@[reducible, inline]
abbrev List.contains {α : Type u} [BEq α] (as : List α) (a : α) :

O(|l|). elem a l or l.contains a is true if there is an element in l equal to a.

• elem 3 [1, 4, 2, 3, 3, 7] = true
• elem 5 [1, 4, 2, 3, 3, 7] = false
Equations
Instances For
@[simp]
theorem List.contains_nil {α : Type u} {a : α} [BEq α] :
[].contains a = false

### Mem #

inductive List.Mem {α : Type u} (a : α) :
List αProp

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 asList.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
instance List.instMembership {α : Type u} :
Equations
• List.instMembership = { mem := List.Mem }
theorem List.mem_of_elem_eq_true {α : Type u} [BEq α] [] {a : α} {as : List α} :
List.elem a as = truea as
theorem List.elem_eq_true_of_mem {α : Type u} [BEq α] [] {a : α} {as : List α} (h : a as) :
instance List.instDecidableMemOfLawfulBEq {α : Type u} [BEq α] [] (a : α) (as : List α) :
Decidable (a as)
Equations
theorem List.mem_append_of_mem_left {α : Type u} {a : α} {as : List α} (bs : List α) :
a asa as ++ bs
theorem List.mem_append_of_mem_right {α : Type u} {b : α} {bs : List α} (as : List α) :
b bsb as ++ bs
instance List.decidableBEx {α : Type u} (p : αProp) [] (l : List α) :
Decidable (∃ (x : α), x l p x)
Equations
instance List.decidableBAll {α : Type u} (p : αProp) [] (l : List α) :
Decidable (∀ (x : α), x lp x)
Equations

## Sublists #

### take #

def List.take {α : Type u} :
NatList αList α

O(min n |xs|). Returns the first n elements of xs, or the whole list if n is too large.

• take 0 [a, b, c, d, e] = []
• take 3 [a, b, c, d, e] = [a, b, c]
• take 6 [a, b, c, d, e] = [a, b, c, d, e]
Equations
Instances For
@[simp]
theorem List.take_nil {α : Type u} {i : Nat} :
List.take i [] = []
@[simp]
theorem List.take_zero {α : Type u} (l : List α) :
= []
@[simp]
theorem List.take_cons_succ :
∀ {α : Type u_1} {a : α} {as : List α} {i : Nat}, List.take (i + 1) (a :: as) = a :: List.take i as

### drop #

def List.drop {α : Type u} :
NatList αList α

O(min n |xs|). Removes the first n elements of xs.

• drop 0 [a, b, c, d, e] = [a, b, c, d, e]
• drop 3 [a, b, c, d, e] = [d, e]
• drop 6 [a, b, c, d, e] = []
Equations
Instances For
@[simp]
theorem List.drop_nil {α : Type u} {i : Nat} :
List.drop i [] = []
@[simp]
theorem List.drop_zero {α : Type u} (l : List α) :
= l
@[simp]
theorem List.drop_succ_cons :
∀ {α : Type u_1} {a : α} {l : List α} {n : Nat}, List.drop (n + 1) (a :: l) =
theorem List.drop_eq_nil_of_le {α : Type u} {as : List α} {i : Nat} (h : as.length i) :
List.drop i as = []

### takeWhile #

def List.takeWhile {α : Type u} (p : αBool) (xs : List α) :
List α

O(|xs|). Returns the longest initial segment of xs for which p returns true.

Equations
Instances For
@[simp]
theorem List.takeWhile_nil {α : Type u} {p : αBool} :
= []

### dropWhile #

def List.dropWhile {α : Type u} (p : αBool) :
List αList α

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
Instances For
@[simp]
theorem List.dropWhile_nil {α : Type u} {p : αBool} :
= []

### partition #

@[inline]
def List.partition {α : Type u} (p : αBool) (as : List α) :
List α × List α

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
Instances For
@[specialize #[]]
def List.partition.loop {α : Type u} (p : αBool) :
List αList α × List αList α × List α
Equations
Instances For

### dropLast #

def List.dropLast {α : Type u_1} :
List αList α

Removes the last element of the list.

Equations
• [].dropLast = []
• (a :: as).dropLast = a :: as.dropLast
Instances For
@[simp]
theorem List.dropLast_nil {α : Type u} :
[].dropLast = []
@[simp]
theorem List.dropLast_single :
∀ {α : Type u_1} {x : α}, [x].dropLast = []
@[simp]
theorem List.dropLast_cons₂ :
∀ {α : Type u_1} {x y : α} {zs : List α}, (x :: y :: zs).dropLast = x :: (y :: zs).dropLast
@[simp]
theorem List.length_dropLast_cons {α : Type u} (a : α) (as : List α) :
(a :: as).dropLast.length = as.length

### isPrefixOf #

def List.isPrefixOf {α : Type u} [BEq α] :
List αList αBool

isPrefixOf l₁ l₂ returns true Iff l₁ is a prefix of l₂. That is, there exists a t such that l₂ == l₁ ++ t.

Equations
• [].isPrefixOf x = true
• x.isPrefixOf [] = false
• (a :: as).isPrefixOf (b :: bs) = (a == b && as.isPrefixOf bs)
Instances For
@[simp]
theorem List.isPrefixOf_nil_left {α : Type u} {l : List α} [BEq α] :
[].isPrefixOf l = true
@[simp]
theorem List.isPrefixOf_cons_nil {α : Type u} {a : α} {as : List α} [BEq α] :
(a :: as).isPrefixOf [] = false
theorem List.isPrefixOf_cons₂ {α : Type u} {as : List α} {b : α} {bs : List α} [BEq α] {a : α} :
(a :: as).isPrefixOf (b :: bs) = (a == b && as.isPrefixOf bs)

### isPrefixOf? #

def List.isPrefixOf? {α : Type u} [BEq α] :
List αList αOption (List α)

isPrefixOf? l₁ l₂ returns some t when l₂ == l₁ ++ t.

Equations
• [].isPrefixOf? x = some x
• x.isPrefixOf? [] = none
• (a :: as).isPrefixOf? (b :: bs) = if (a == b) = true then as.isPrefixOf? bs else none
Instances For

### isSuffixOf #

def List.isSuffixOf {α : Type u} [BEq α] (l₁ : List α) (l₂ : List α) :

isSuffixOf l₁ l₂ returns true Iff l₁ is a suffix of l₂. That is, there exists a t such that l₂ == t ++ l₁.

Equations
• l₁.isSuffixOf l₂ = l₁.reverse.isPrefixOf l₂.reverse
Instances For
@[simp]
theorem List.isSuffixOf_nil_left {α : Type u} {l : List α} [BEq α] :
[].isSuffixOf l = true

### isSuffixOf? #

def List.isSuffixOf? {α : Type u} [BEq α] (l₁ : List α) (l₂ : List α) :

isSuffixOf? l₁ l₂ returns some t when l₂ == t ++ l₁.

Equations
• l₁.isSuffixOf? l₂ = Option.map List.reverse (l₁.reverse.isPrefixOf? l₂.reverse)
Instances For

### rotateLeft #

def List.rotateLeft {α : Type u} (xs : List α) (n : ) :
List α

O(n). Rotates the elements of xs to the left such that the element at xs[i] rotates to xs[(i - n) % l.length].

Equations
• xs.rotateLeft n = let len := xs.length; if len 1 then xs else let n := n % len; let b := List.take n xs; let e := List.drop n xs; e ++ b
Instances For
@[simp]
theorem List.rotateLeft_nil {α : Type u} {n : Nat} :
[].rotateLeft n = []

### rotateRight #

def List.rotateRight {α : Type u} (xs : List α) (n : ) :
List α

O(n). Rotates the elements of xs to the right such that the element at xs[i] rotates to xs[(i + n) % l.length].

Equations
• xs.rotateRight n = let len := xs.length; if len 1 then xs else let n := len - n % len; let b := List.take n xs; let e := List.drop n xs; e ++ b
Instances For
@[simp]
theorem List.rotateRight_nil {α : Type u} {n : Nat} :
[].rotateRight n = []

## Manipulating elements #

### replace #

def List.replace {α : Type u} [BEq α] :
List αααList α

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
• [].replace x✝ x = []
• (a :: as).replace x✝ x = match x✝ == a with | true => x :: as | false => a :: as.replace x✝ x
Instances For
@[simp]
theorem List.replace_nil {α : Type u} {a : α} {b : α} [BEq α] :
[].replace a b = []
theorem List.replace_cons {α : Type u} {as : List α} {b : α} {c : α} [BEq α] {a : α} :
(a :: as).replace b c = match b == a with | true => c :: as | false => a :: as.replace b c

### insert #

@[inline]
def List.insert {α : Type u} [BEq α] (a : α) (l : List α) :
List α

Inserts an element into a list without duplication.

Equations
Instances For

### erase #

def List.erase {α : Type u_1} [BEq α] :
List ααList α

O(|l|). erase l a removes the first occurrence of a from l.

• erase [1, 5, 3, 2, 5] 5 = [1, 3, 2, 5]
• erase [1, 5, 3, 2, 5] 6 = [1, 5, 3, 2, 5]
Equations
• [].erase x = []
• (a :: as).erase x = match a == x with | true => as | false => a :: as.erase x
Instances For
@[simp]
theorem List.erase_nil {α : Type u} [BEq α] (a : α) :
[].erase a = []
theorem List.erase_cons {α : Type u} [BEq α] (a : α) (b : α) (l : List α) :
(b :: l).erase a = if (b == a) = true then l else b :: l.erase a

### eraseIdx #

def List.eraseIdx {α : Type u} :
List αNatList α

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
• [].eraseIdx x = []
• (head :: as).eraseIdx 0 = as
• (a :: as).eraseIdx n.succ = a :: as.eraseIdx n
Instances For
@[simp]
theorem List.eraseIdx_nil {α : Type u} {i : Nat} :
[].eraseIdx i = []
@[simp]
theorem List.eraseIdx_cons_zero :
∀ {α : Type u_1} {a : α} {as : List α}, (a :: as).eraseIdx 0 = as
@[simp]
theorem List.eraseIdx_cons_succ :
∀ {α : Type u_1} {a : α} {as : List α} {i : Nat}, (a :: as).eraseIdx (i + 1) = a :: as.eraseIdx i

### find? #

def List.find? {α : Type u} (p : αBool) :
List α

O(|l|). find? p l returns the first element for which p returns true, or none if no such element is found.

• find? (· < 5) [7, 6, 5, 8, 1, 2, 6] = some 1
• find? (· < 1) [7, 6, 5, 8, 1, 2, 6] = none
Equations
Instances For
@[simp]
theorem List.find?_nil {α : Type u} {p : αBool} :
List.find? p [] = none
theorem List.find?_cons :
∀ {α : Type u_1} {a : α} {as : List α} {p : αBool}, List.find? p (a :: as) = match p a with | true => some a | false => List.find? p as

### findSome? #

def List.findSome? {α : Type u} {β : Type v} (f : α) :
List α

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
Instances For
@[simp]
theorem List.findSome?_nil {α : Type u} :
∀ {α_1 : Type u_1} {f : αOption α_1}, = none
theorem List.findSome?_cons {α : Type u} {β : Type v} {a : α} {as : List α} {f : α} :
List.findSome? f (a :: as) = match f a with | some b => some b | none =>

### lookup #

def List.lookup {α : Type u} {β : Type v} [BEq α] :
αList (α × β)

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.

• lookup 3 [(1, 2), (3, 4), (3, 5)] = some 4
• lookup 2 [(1, 2), (3, 4), (3, 5)] = none
Equations
Instances For
@[simp]
theorem List.lookup_nil {α : Type u} {β : Type v} {a : α} [BEq α] :
List.lookup a [] = none
theorem List.lookup_cons {α : Type u} :
∀ {β : Type u_1} {b : β} {es : List (α × β)} {a : α} [inst : BEq α] {k : α}, List.lookup a ((k, b) :: es) = match a == k with | true => some b | false => List.lookup a es

## Logical operations #

### any #

def List.any {α : Type u} :
List α(αBool)Bool

O(|l|). Returns true if p is true for any element of l.

• any p [a, b, c] = p a || p b || p c

Short-circuits upon encountering the first true.

Equations
Instances For
@[simp]
theorem List.any_nil :
∀ {α : Type u_1} {f : αBool}, [].any f = false
@[simp]
theorem List.any_cons :
∀ {α : Type u_1} {a : α} {l : List α} {f : αBool}, (a :: l).any f = (f a || l.any f)

### all #

def List.all {α : Type u} :
List α(αBool)Bool

O(|l|). Returns true if p is true for every element of l.

• all p [a, b, c] = p a && p b && p c

Short-circuits upon encountering the first false.

Equations
Instances For
@[simp]
theorem List.all_nil :
∀ {α : Type u_1} {f : αBool}, [].all f = true
@[simp]
theorem List.all_cons :
∀ {α : Type u_1} {a : α} {l : List α} {f : αBool}, (a :: l).all f = (f a && l.all f)

### or #

def List.or (bs : ) :

O(|l|). Returns true if true is an element of the list of booleans l.

• or [a, b, c] = a || b || c
Equations
• bs.or = bs.any id
Instances For
@[simp]
theorem List.or_nil :
[].or = false
@[simp]
theorem List.or_cons {a : Bool} {l : } :
(a :: l).or = (a || l.or)

### and #

def List.and (bs : ) :

O(|l|). Returns true if every element of l is the value true.

• and [a, b, c] = a && b && c
Equations
• bs.and = bs.all id
Instances For
@[simp]
theorem List.and_nil :
[].and = true
@[simp]
theorem List.and_cons {a : Bool} {l : } :
(a :: l).and = (a && l.and)

## Zippers #

### zipWith #

@[specialize #[]]
def List.zipWith {α : Type u} {β : Type v} {γ : Type w} (f : αβγ) (xs : List α) (ys : List β) :
List γ

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
Instances For
@[simp]
theorem List.zipWith_nil_left {α : Type u} {β : Type v} {γ : Type w} {l : List β} {f : αβγ} :
List.zipWith f [] l = []
@[simp]
theorem List.zipWith_nil_right {α : Type u} {β : Type v} {γ : Type w} {l : List α} {f : αβγ} :
List.zipWith f l [] = []
@[simp]
theorem List.zipWith_cons_cons {α : Type u} {β : Type v} {γ : Type w} {a : α} {as : List α} {b : β} {bs : List β} {f : αβγ} :
List.zipWith f (a :: as) (b :: bs) = f a b :: List.zipWith f as bs

### zip #

def List.zip {α : Type u} {β : Type v} :
List αList βList (α × β)

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
Instances For
@[simp]
theorem List.zip_nil_left {α : Type u} {β : Type v} {l : List β} :
[].zip l = []
@[simp]
theorem List.zip_nil_right {α : Type u} {β : Type v} {l : List α} :
l.zip [] = []
@[simp]
theorem List.zip_cons_cons :
∀ {α : Type u_1} {a : α} {as : List α} {α_1 : Type u_2} {b : α_1} {bs : List α_1}, (a :: as).zip (b :: bs) = (a, b) :: as.zip bs

### zipWithAll #

def List.zipWithAll {α : Type u} {β : Type v} {γ : Type w} (f : γ) :
List αList βList γ

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
Instances For
@[simp]
theorem List.zipWithAll_nil_right :
∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : Option α_1α_2} {as : List α}, List.zipWithAll f as [] = List.map (fun (a : α) => f (some a) none) as
@[simp]
theorem List.zipWithAll_nil_left :
∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : Option α_1α_2} {bs : List α_1}, List.zipWithAll f [] bs = List.map (fun (b : α_1) => f none (some b)) bs
@[simp]
theorem List.zipWithAll_cons_cons :
∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : Option α_1α_2} {a : α} {as : List α} {b : α_1} {bs : List α_1}, List.zipWithAll f (a :: as) (b :: bs) = f (some a) (some b) :: List.zipWithAll f as bs

### unzip #

def List.unzip {α : Type u} {β : Type v} :
List (α × β)List α × List β

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
• [].unzip = ([], [])
• ((a, b) :: t).unzip = match t.unzip with | (al, bl) => (a :: al, b :: bl)
Instances For
@[simp]
theorem List.unzip_nil {α : Type u} {β : Type v} :
[].unzip = ([], [])
@[simp]
theorem List.unzip_cons {α : Type u} {β : Type v} {t : List (α × β)} {h : α × β} :
(h :: t).unzip = match t.unzip with | (al, bl) => (h.fst :: al, h.snd :: bl)

## Ranges and enumeration #

### range #

def List.range (n : Nat) :

O(n). range n is the numbers from 0 to n exclusive, in increasing order.

• range 5 = [0, 1, 2, 3, 4]
Equations
Instances For
Equations
Instances For
@[simp]
theorem List.range_zero :
= []

### iota #

def List.iota :

O(n). iota n is the numbers from 1 to n inclusive, in decreasing order.

• iota 5 = [5, 4, 3, 2, 1]
Equations
Instances For
@[simp]
theorem List.iota_zero :
= []
@[simp]
theorem List.iota_succ {i : Nat} :
List.iota (i + 1) = (i + 1) ::

### enumFrom #

def List.enumFrom {α : Type u} :
NatList αList (Nat × α)

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
Instances For
@[simp]
theorem List.enumFrom_nil {α : Type u} {i : Nat} :
= []
@[simp]
theorem List.enumFrom_cons :
∀ {α : Type u_1} {a : α} {as : List α} {i : Nat}, List.enumFrom i (a :: as) = (i, a) :: List.enumFrom (i + 1) as

### enum #

def List.enum {α : Type u} :
List αList (Nat × α)

O(|l|). enum l pairs up each element with its index in the list.

• enum [a, b, c] = [(0, a), (1, b), (2, c)]
Equations
• List.enum =
Instances For
@[simp]
theorem List.enum_nil {α : Type u} :
[].enum = []

## Minima and maxima #

### minimum? #

def List.minimum? {α : Type u} [Min α] :
List α

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

Equations
Instances For

### maximum? #

def List.maximum? {α : Type u} [Max α] :
List α

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

Equations
Instances For

## Other list operations #

The functions are currently mostly used in meta code, and do not have sufficient API developed for verification work.

### intersperse #

def List.intersperse {α : Type u} (sep : α) :
List αList α

O(|l|). intersperse sep l alternates sep and the elements of l:

Equations
Instances For
@[simp]
theorem List.intersperse_nil {α : Type u} (sep : α) :
@[simp]
theorem List.intersperse_single {α : Type u} {x : α} (sep : α) :
List.intersperse sep [x] = [x]
@[simp]
theorem List.intersperse_cons₂ {α : Type u} {x : α} {y : α} {zs : List α} (sep : α) :
List.intersperse sep (x :: y :: zs) = x :: sep :: List.intersperse sep (y :: zs)

### intercalate #

def List.intercalate {α : Type u} (sep : List α) (xs : List (List α)) :
List α

O(|xs|). intercalate sep xs alternates sep and the elements of xs:

Equations
Instances For

### eraseDups #

def List.eraseDups {α : Type u_1} [BEq α] (as : List α) :
List α

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
• as.eraseDups =
Instances For
def List.eraseDups.loop {α : Type u_1} [BEq α] :
List αList αList α
Equations
Instances For

### eraseReps #

def List.eraseReps {α : Type u_1} [BEq α] :
List αList α

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
Instances For
def List.eraseReps.loop {α : Type u_1} [BEq α] :
αList αList αList α
Equations
Instances For

### span #

@[inline]
def List.span {α : Type u} (p : αBool) (as : List α) :
List α × List α

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
Instances For
@[specialize #[]]
def List.span.loop {α : Type u} (p : αBool) :
List αList αList α × List α
Equations
Instances For

### groupBy #

@[specialize #[]]
def List.groupBy {α : Type u} (R : ααBool) :
List αList (List α)

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
Instances For
@[specialize #[]]
def List.groupBy.loop {α : Type u} (R : ααBool) :
List ααList αList (List α)List (List α)
Equations
Instances For

### removeAll #

def List.removeAll {α : Type u} [BEq α] (xs : List α) (ys : List α) :
List α

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
Instances For