List-like structures

InductiveList#

Linked lists: ordered lists, in which each element has a reference to the next element.

Most operations on linked lists take time proportional to the length of the list, because each element must be traversed to find the next element.

List α is isomorphic to Array α, but they are useful for different things: * List α is easier for reasoning, and Array α is modeled as a wrapper around List α. * List α works well as a persistent data structure, when many copies of the tail are shared. When the value is not shared, Array α will have better performance because it can do destructive updates.

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

Sources

• Mathlib documentation: List
• Mathlib overview: Data structures › List-like structures

MathlibList

Used by 19

Used byThe Denumerability of the Rational Numbers · Königsberg Bridges Problem · The Solution of the General Quartic Equation · Divisibility by 3 Rule · Dyck words · Array · Difference list · Key-value map · Multiset · Tensor product · Language · Cantor normal form · Epsilon numbers · Gamma numbers · Nielsen–Schreier theorem · Kleene's recursion theorem · Tietze extension theorem · Zeckendorf's theorem · Differentiability of the limit of a sequence of functions

StructureArray#

Array α is the type of dynamic arrays with elements from α. This type has special support in the runtime.

Arrays perform best when unshared. As long as there is never more than one reference to an array, all updates will be performed destructively. This results in performance comparable to mutable arrays in imperative programming languages.

An array has a size and a capacity. The size is the number of elements present in the array, while the capacity is the amount of memory currently allocated for elements. The size is accessible via Array.size, but the capacity is not observable from Lean code. Array.emptyWithCapacity n creates an array which is equal to #[], but internally allocates an array of capacity n. When the size exceeds the capacity, allocation is required to grow the array.

From the point of view of proofs, Array α is just a wrapper around List α.

Array.{u} (α : Type u) : Type u

Sources

• Mathlib documentation: Array
• Mathlib overview: Data structures › List-like structures

MathlibArray

Uses 1 · Used by 2

Statement usesList

Used byHash map · Ostrowski's theorem

StructureDifference list#

A difference List is a Function that, given a List, returns the original contents of the difference List prepended to the given List. This structure supports O(1) append and push operations on lists, making it useful for append-heavy uses such as logging and pretty printing.

Batteries.DList.{u} (α : Type u) : Type u

Sources

• Mathlib documentation: Batteries.DList
• Mathlib overview: Data structures › List-like structures

MathlibBatteries.DList

Uses 1

Statement usesList

DefinitionLazy list#

A monadic lazy list, controlled by an arbitrary monad.

MLList.{u} (m : Type u → Type u) (α : Type u) : Type u

Sources

• Mathlib documentation: MLList
• Mathlib overview: Data structures › List-like structures

MathlibMLList

DefinitionStream#

A stream Stream' α is an infinite sequence of elements of α.

Stream'.{u} (α : Type u) : Type u

Sources

• Mathlib documentation: Stream'
• Source of Stream' in Mathlib/Data/Stream/Defs.lean
• Mathlib overview: Data structures › List-like structures

MathlibStream'

Uses 1 · Used by 3

Statement usesNatural number

Used byHindman's theorem (Ramsey theory) · Sequence · Hindman's theorem (1000+ theorems)

DefinitionSequence#

Seq α is the type of possibly infinite lists (referred here as sequences). It is encoded as an infinite stream of options such that if f n = none, then f m = none for all m ≥ n.

Stream'.Seq.{u} (α : Type u) : Type u

Sources

• Mathlib documentation: Stream'.Seq
• Source of Stream'.Seq in Mathlib/Data/Seq/Defs.lean
• Mathlib overview: Data structures › List-like structures

MathlibStream'.Seq

Uses 1 · Used by 2

Statement usesStream

Used byWeak sequence · Continued fraction

DefinitionWeak sequence#

Weak sequences.

While the Seq structure allows for lists which may not be finite, a weak sequence also allows the computation of each element to involve an indeterminate amount of computation, including possibly an infinite loop. This is represented as a regular Seq interspersed with none elements to indicate that computation is ongoing.

This model is appropriate for Haskell style lazy lists, and is closed under most interesting computation patterns on infinite lists, but conversely it is difficult to extract elements from it.

Stream'.WSeq.{u_1} (α : Type u_1) : Type u_1

Sources

• Mathlib documentation: Stream'.WSeq
• Source of Stream'.WSeq in Mathlib/Data/WSeq/Basic.lean
• Mathlib overview: Data structures › List-like structures

MathlibStream'.WSeq

Uses 1

Statement usesSequence

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.