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

Conventions for notations in identifiers:

• The recommended spelling of <+: in identifiers is prefix (not isPrefix).

term ::= ...
    | `IsPrefix l₁ l₂`, or `l₁ <+: l₂`, means that `l₁` is a prefix of `l₂`,
that is, `l₂` has the form `l₁ ++ t` for some `t`.


Conventions for notations in identifiers:

 * The recommended spelling of `<+:` in identifiers is `prefix` (not `isPrefix`).term <+: term

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

Conventions for notations in identifiers:

• The recommended spelling of <+: in identifiers is prefix (not isPrefix).

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

Conventions for notations in identifiers:

• The recommended spelling of <:+ in identifiers is suffix (not isSuffix).

term ::= ...
    | `IsSuffix l₁ l₂`, or `l₁ <:+ l₂`, means that `l₁` is a suffix of `l₂`,
that is, `l₂` has the form `t ++ l₁` for some `t`.


Conventions for notations in identifiers:

 * The recommended spelling of `<:+` in identifiers is `suffix` (not `isSuffix`).term <:+ term

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

Conventions for notations in identifiers:

• The recommended spelling of <:+ in identifiers is suffix (not isSuffix).

IsInfix 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.

Conventions for notations in identifiers:

• The recommended spelling of <:+: in identifiers is infix (not isInfix).

term ::= ...
    | `IsInfix 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`.


Conventions for notations in identifiers:

 * The recommended spelling of `<:+:` in identifiers is `infix` (not `isInfix`).term <:+: term

IsInfix 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.

Conventions for notations in identifiers:

• The recommended spelling of <:+: in identifiers is infix (not isInfix).

Perm l₁ l₂ or l₁ ~ l₂ asserts that l₁ and l₂ are permutations of each other. This is defined by induction using pairwise swaps.

Constructors

nil.{u} {α : Type u} : [].Perm []

cons.{u} {α : Type u} (x : α) {l₁ l₂ : List α} :
  l₁.Perm l₂ → (x :: l₁).Perm (x :: l₂)

swap.{u} {α : Type u} (x y : α) (l : List α) :
  (y :: x :: l).Perm (x :: y :: l)

trans.{u} {α : Type u} {l₁ l₂ l₃ : List α} :
  l₁.Perm l₂ → l₂.Perm l₃ → l₁.Perm l₃

term ::= ...
    | `Perm l₁ l₂` or `l₁ ~ l₂` asserts that `l₁` and `l₂` are permutations
of each other. This is defined by induction using pairwise swaps.
term ~ term

Perm l₁ l₂ or l₁ ~ l₂ asserts that l₁ and l₂ are permutations of each other. This is defined by induction using pairwise swaps.

This syntax is only available when the List namespace is opened.

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

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

Constructors

nil.{u} {α : Type u} {R : α → α → Prop} : List.Pairwise R []

cons.{u} {α : Type u} {R : α → α → Prop} {a : α}
  {l : List α} :
  (∀ (a' : α), a' ∈ l → R a a') →
    List.Pairwise R l → List.Pairwise R (a :: l)

Nodup l means that l has no duplicates, that is, any element appears at most once in the List. It is defined as Pairwise (≠).

Lexicographic ordering for lists.

Constructors

nil.{u} {α : Type u} {r : α → α → Prop} {a : α}
  {l : List α} : List.Lex r [] (a :: l)

cons.{u} {α : Type u} {r : α → α → Prop} {a : α}
  {l₁ l₂ : List α} (h : List.Lex r l₁ l₂) :
  List.Lex r (a :: l₁) (a :: l₂)

rel.{u} {α : Type u} {r : α → α → Prop} {a₁ : α}
  {l₁ : List α} {a₂ : α} {l₂ : List α} (h : r a₁ a₂) :
  List.Lex r (a₁ :: l₁) (a₂ :: l₂)

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

Constructors

head.{u} {α : Type u} {a : α} (as : List α) :
  List.Mem a (a :: as)

tail.{u} {α : Type u} {a : α} (b : α) {as : List α} :
  List.Mem a as → List.Mem a (b :: as)

singleton x = [x].

l.concat a appends a at the end of l, that is, l ++ [a].

replicate n a is n copies of a:

• replicate 5 a = [a, a, a, a, a]

Tail-recursive version of List.replicate.

ofFn f with f : fin n → α returns the list whose ith element is f i

ofFn f = [f 0, f 1, ... , f (n - 1)]

O(|xs|): append two lists. [1, 2, 3] ++ [4, 5] = [1, 2, 3, 4, 5]. It takes time proportional to the first 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.

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

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

range' start len step is the list of numbers [start, start+step, ..., start+(len-1)*step]. It is intended mainly for proving properties of range and iota.

Optimized version of range'.

finRange n lists all elements of Fin n in order

The length of a list: [].length = 0 and (a :: l).length = l.length + 1.

This function is overridden in the compiler to lengthTR, which uses constant stack space, while leaving this function to use the "naive" recursion which is easier for reasoning.

A tail-recursive version of List.length, used to implement List.length without running out of stack space.

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

• isEmpty [] = true

• isEmpty [a] = false

• isEmpty [a, b] = false

Returns the first element of a non-empty list.

Returns the first element in the list.

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

Returns the first element in the list.

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

Returns the first element in the list.

If the list is empty, this function panics when executed, and returns default. See head and headD for safer alternatives.

Get the tail of a nonempty list, or return [] for [].

Drops the first element of the list.

If the list is empty, this function panics when executed, and returns the empty list. See tail and tailD for safer alternatives.

Drops the first element of the list.

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

Drops the first element of the list.

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

as.get i returns the i'th element of the list as. This version of the function uses i : Fin as.length to ensure that it will not index out of bounds.

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!.

Returns the last element of a non-empty list.

Returns the last element in the list.

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

Returns the last element in the list.

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

Returns the last element in the list.

If the list is empty, this function panics when executed, and returns default. See getLast and getLastD for safer alternatives.

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

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

• [].max? = none

• [4].max? = some 4

• [1, 4, 2, 10, 6].max? = some 10

The maximum absolute value in a list of integers.

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

• [].min? = none

• [4].min? = some 4

• [1, 4, 2, 10, 6].min? = some 1

The minimum absolute value of a nonzero entry, or zero if all entries are zero.

We completely characterize the function via minNatAbs_eq_zero_iff and minNatAbs_eq_nonzero_iff below.

The minimum non-zero entry in a list of natural numbers, or zero if all entries are zero.

We completely characterize the function via nonzeroMinimum_eq_zero_iff and nonzeroMinimum_eq_nonzero_iff below.

Converts a List α into an Array α. (This is preferred over the synonym Array.mk.)

At runtime, this constructor is implemented by List.toArrayImpl and is O(n) in the length of the list.

Convert a List α into an Array α. This is O(n) in the length of the list.

l.set n a sets the value of list l at (zero-based) index n to a: [a, b, c, d].set 1 b' = [a, b', c, d]

Tail recursive version of List.set.

Apply f to the nth element of the list, if it exists, replacing that element with the result.

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

Tail-recursive version of modify.

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.

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]

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]

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]

Tail recursive version of List.eraseIdx.

eraseP p l removes the first element of l satisfying the predicate p.

Tail-recursive version of eraseP.

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]

Tail recursive version of List.erase.

extract l start stop returns the slice of l from indices start to stop (exclusive).

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]

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]

Tail recursive version of List.replace.

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.

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

• flatten [[a], [], [b, c], [d, e, f]] = [a, b, c, d, e, f]

Tail recursive version of List.flatten.

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

• rotateLeft [1, 2, 3, 4, 5] 3 = [4, 5, 1, 2, 3]

• rotateLeft [1, 2, 3, 4, 5] 5 = [1, 2, 3, 4, 5]

• rotateLeft [1, 2, 3, 4, 5] = [2, 3, 4, 5, 1]

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

• rotateRight [1, 2, 3, 4, 5] 3 = [3, 4, 5, 1, 2]

• rotateRight [1, 2, 3, 4, 5] 5 = [1, 2, 3, 4, 5]

• rotateRight [1, 2, 3, 4, 5] = [5, 1, 2, 3, 4]

Pads l : List α on the left with repeated occurrences of a : α until it is of length n. If l is initially larger than n, just return l.

Optimized version of leftpad.

Pads l : List α on the right with repeated occurrences of a : α until it is of length n. If l is initially larger than n, just return l.

Simplified implementation of stable merge sort.

This function is designed for reasoning about the algorithm, and is not efficient. (It particular it uses the non tail-recursive merge function, and so can not be run on large lists, but also makes unnecessary traversals of lists.) It is replaced at runtime in the compiler by mergeSortTR₂ using a @[csimp] lemma.

Because we want the sort to be stable, it is essential that we split the list in two contiguous sublists.

O(min |l| |r|). Merge two lists using le as a switch.

This version is not tail-recursive, but it is replaced at runtime by mergeTR using a @[csimp] lemma.

Applies the applicative action f on every element in the list, left-to-right.

NB: If m is also a Monad, then using forM can be more efficient.

See List.mapA for the variant that collects results. See List.forM for the variant that works with Monad.

Applies the monadic action f on every element in the list, left-to-right.

See List.mapM for the variant that collects results. See List.forA for the variant that works with Applicative.

Maps f over the list and collects the results with <|>.

Sum of a list.

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

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

• map f [a, b, c] = [f a, f b, f c]

Tail-recursive version of List.map.

Applies the monadic action f on every element in the list, left-to-right, and returns the list of results.

See List.forM for the variant that discards the results. See List.mapA for the variant that works with Applicative.

Alternate (non-tail-recursive) form of mapM for proofs.

Note that we can not have this as the main definition and replace it using a @[csimp] lemma, because they are only equal when m is a LawfulMonad.

Applies the applicative action f on every element in the list, left-to-right, and returns the list of results.

NB: If m is also a Monad, then using mapM can be more efficient.

See List.forA for the variant that discards the results. See List.mapM for the variant that works with Monad.

Warning: this function is not tail-recursive, meaning that it may fail with a stack overflow on long lists.

Given a list as = [a₀, a₁, ...] and a function f : (i : Nat) → α → (h : i < as.length) → β, returns the list [f 0 a₀ ⋯, f 1 a₁ ⋯, ...].

Given a list as = [a₀, a₁, ...] and a monadic function f : (i : Nat) → α → (h : i < as.length) → m β, returns the list [f 0 a₀ ⋯, f 1 a₁ ⋯, ...].

Given a function f : Nat → α → β and as : List α, as = [a₀, a₁, ...], returns the list [f 0 a₀, f 1 a₁, ...].

Given a monadic function f : Nat → α → m β and as : List α, as = [a₀, a₁, ...], returns the list [f 0 a₀, f 1 a₁, ...].

Monomorphic List.mapM. The internal implementation uses pointer equality, and does not allocate a new list if the result of each f a is a pointer equal value a.

flatMap xs f 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]

Applies the monadic function f on every element x in the list, left-to-right, and returns the concatenation of the results.

Tail recursive version of List.flatMap.

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₃])

Tail recursive version of List.unzip.

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₃)]

O(|l|). zipIdx l zips a list with its indices, optionally starting from a given index.

• zipIdx [a, b, c] = [(a, 0), (b, 1), (c, 2)]

• zipIdx [a, b, c] 5 = [(a, 5), (b, 6), (c, 7)]

Tail recursive version of List.zipIdx.

Given an ordering relation le : α → α → Bool, construct the lexicographic ordering on α × Nat. which first compares the first components using le, but if these are equivalent (in the sense le a.2 b.2 && le b.2 a.2) then compares the second components using ≤.

This function is only used in stating the stability properties of mergeSort.

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₃]

Tail recursive version of List.zipWith.

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.

O(|l|). filter f l returns the list of elements in l for which f returns true.

Tail-recursive version of List.filter.

Applies the monadic predicate p on every element in the list, left-to-right, and returns those elements x for which p x returns true.

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.

Tail recursive version of filterMap.

Applies the monadic function f on every element x in the list, left-to-right, and returns those results y for which f x returns some y.

Applies the monadic predicate p on every element in the list, right-to-left, and returns those elements x for which p x returns true.

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]

Tail recursive version of List.take.

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

• takeWhile (· > 5) [7, 6, 4, 8] = [7, 6]

• takeWhile (· > 5) [7, 6, 6, 8] = [7, 6, 6, 8]

Tail recursive version of List.takeWhile.

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] = []

Removes the last element of the list.

• dropLast [] = []

• dropLast [a] = []

• dropLast [a, b, c] = [a, b]

Tail recursive version of dropLast.

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.

Split a list at an index.

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])

O(|l|). splitBy R l splits l into chains of elements such that adjacent elements are related by R.

• splitBy (·==·) [1, 1, 2, 2, 2, 3, 2] = [[1, 1], [2, 2, 2], [3], [2]]

• splitBy (·<·) [1, 2, 5, 4, 5, 1, 4] = [[1, 2, 5], [4, 5], [1, 4]]

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.