Maps

StructureKey-value map#

AList β is a key-value map stored as a List (i.e. a linked list). It is a wrapper around certain List functions with the added constraint that the list have unique keys.

AList.{u, v} {α : Type u} (β : α → Type v) : Type (max u v)

Sources

• Mathlib documentation: AList
• Source of AList in Mathlib/Data/List/AList.lean
• Mathlib overview: Data structures › Maps

MathlibAList

Uses 1

Statement usesList

StructureHash map#

Hash maps.

This is a simple separate-chaining hash table. The data of the hash map consists of a cached size and an array of buckets, where each bucket is a linked list of key-value pairs. The number of buckets is always a power of two. The hash map doubles its size upon inserting an element such that the number of elements is more than 75% of the number of buckets.

The hash table is backed by an Array. Users should make sure that the hash map is used linearly to avoid expensive copies.

The hash map uses == (provided by the BEq typeclass) to compare keys and hash (provided by the Hashable typeclass) to hash them. To ensure that the operations behave as expected, == should be an equivalence relation and a == b should imply hash a = hash b (see also the EquivBEq and LawfulHashable typeclasses). Both of these conditions are automatic if the BEq instance is lawful, i.e., if a == b implies a = b.

These hash maps contain a bundled well-formedness invariant, which means that they cannot be used in nested inductive types. For these use cases, Std.Data.HashMap.Raw and Std.Data.HashMap.Raw.WF unbundle the invariant from the hash map. When in doubt, prefer HashMap over HashMap.Raw.

Dependent hash maps, in which keys may occur in their values' types, are available as Std.Data.DHashMap.

Std.HashMap.{u, v} (α : Type u) (β : Type v) [BEq α] [Hashable α] : Type (max u v)

Sources

• Mathlib documentation: Std.HashMap
• Mathlib overview: Data structures › Maps

MathlibStd.HashMap

Uses 2

Statement usesArray · Natural number

StructureFinitely supported function#

Finsupp α M, denoted α →₀ M, is the type of functions f : α → M such that f x = 0 for all but finitely many x.

Finsupp.{u_8, u_9} (α : Type u_8) (M : Type u_9) [Zero M] : Type (max u_8 u_9)

Sources

• Mathlib documentation: Finsupp
• Source of Finsupp in Mathlib/Data/Finsupp/Defs.lean
• Mathlib overview: Data structures › Maps

MathlibFinsupp

Uses 2 · Used by 7

Statement usesFinite set · Natural number

Used byBertrand’s Postulate · Polynomial in one indeterminate · Polynomial in several indeterminates · Structure theorem · Basis · Jacobson density theorem · Linear independence

StructureFinite map#

Finmap β is the type of finite maps over a multiset. It is effectively a quotient of AList β by permutation of the underlying list.

Finmap.{u, v} {α : Type u} (β : α → Type v) : Type (max u v)

Sources

• Mathlib documentation: Finmap
• Source of Finmap in Mathlib/Data/Finmap.lean
• Mathlib overview: Data structures › Maps

MathlibFinmap

Uses 1

Statement usesMultiset

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.