Lean 语言参考

20.19. 地图和套装🔗

map 是将键与值关联起来的数据结构。 它们也称为 dictionaries、associative arrays，或简称为哈希表。

在 Lean 中，地图可能具有以下属性：

表示

映射在内存中的表示可以是树或哈希表。 当共享数据结构的 引用 时，基于树的表示会更好，因为哈希表基于 数组。 当引用不唯一时，数组将在修改时完整复制，而在修改树时只需复制从树根到修改节点的路径。 另一方面，当引用不共享时，哈希表会更有效，因为非共享数组可以在恒定时间内修改。 此外，基于树的映射按顺序存储数据，从而支持数据的有序遍历。

外延性

映射可以被视为从键到值的部分函数。 Extensional 映射 是 命题等价 与此解释匹配的映射。 这可以方便推理，但也排除了一些能够区分它们的有用操作。 一般来说，仅在需要验证时才应使用外延映射。

是否依赖

dependent map 是其中每个值的类型由其对应的键确定的类型，而不是恒定的。 从属地图具有更强的表达能力，但也更难使用。 他们对用户提出了更多要求。 例如，DHashMap 上的许多操作需要 LawfulBEq 实例而不是 BEq。

地图

表示

外延性？

依赖？

TreeMap

树

否

否

DTreeMap

树

否

是的

HashMap

哈希表

否

否

DHashMap

哈希表

否

是的

ExtHashMap

哈希表

是的

否

ExtDHashMap

哈希表

是的

是的

通过将其值类型设置为 Unit，地图始终可以用作集合。 提供了以下集合类型：

  • Std.HashSet是一个基于哈希表的集合。其性能特征类似于Std.HashMap：它基于数组，可以高效更新，但仅限于不共享时。

  • Std.TreeSet是一个基于平衡树的集合。其性能特征类似于Std.TreeMap。

  • Std.ExtHashSet 是一种扩展哈希集类型，它与有限集的数学概念相匹配：如果两个集合包含相同的元素，则它们相等。

20.19.1. 图书馆设计🔗

地图和集合上的所有基本操作都经过充分验证。 对于使用列表实现的更简单的模型，它们被证明是正确的。 同时，地图和集合具有可预测的性能。

某些类型包括尚未完全验证的附加操作。 这些操作很有用，并不是所有程序都需要充分验证。 示例包括 HashMap.partition 和 TreeMap.filterMap。

20.19.1.1. 融合运营🔗

根据表的预先存在的内容修改表是很常见的。 为了避免必须遍历数据结构两次，在“融合”变体中提供了许多查询/修改对，这些变体在修改映射或集合的同时执行查询。 在某些情况下，查询的结果会影响修改。

例如，Std.HashMap 提供 containsThenInsert，它将键值对插入到映射中，同时发出信号通知以前是否已找到该映射；以及 containsThenInsertIfNew，它仅在以前不存在的情况下插入新映射。 alter 函数修改给定键的值，而无需多次搜索该键；交替是由一个函数执行的，其中缺失值由 none 表示。

20.19.1.2. 原始数据和不变量🔗

基于哈希的映射和基于树的映射都依赖于某些内部格式良好的不变量，例如树是平衡和有序的。 在Lean的标准库中，这些数据结构被表示为一对底层数据，并带有其格式良好的证明。 这个事实主要是一个内部实现细节；然而，它与一种情况下的用户相关：这种表示形式阻止它们在 嵌套归纳类型 中使用。

为了使其能够在嵌套归纳类型中使用，标准库提供了每个容器的“raw”变体及其不变量的单独“非捆绑”版本。 它们使用以下命名约定：

  • T.Raw 是 T 类型的版本，没有其不变量。例如，Std.HashMap.Raw 是 Std.HashMap 的一个版本，没有嵌入校样。

  • T.Raw.WF 是相应的格式良好谓词。例如，Std.HashMap.Raw.WF 断言 Std.HashMap.Raw 格式良好。

  • T 上的每个操作（称为 T.f）在 T.Raw 上都有一个对应的操作（称为 T.Raw.f）。例如，Std.HashMap.Raw.insert 是与原始哈希映射一起使用的 Std.HashMap.insert 版本。

  • 每个操作 T.Raw.f 都有一个关联的格式良好引理 T.Raw.WF.f。例如，Std.HashMap.Raw.WF.insert 断言将新的键值对插入到格式良好的原始哈希映射中会产生格式良好的原始哈希映射。

由于绝大多数用例不需要它们，因此并非所有有关原始类型的引理都默认随数据结构导入。 通常需要导入 Std.Data.T.RawLemmas（其中 T 是有问题的数据结构）。

发生在映射或集合内部的嵌套归纳类型应分三个阶段定义：

  1. 首先，定义使用原始版本的映射或集合类型的嵌套归纳类型的原始版本。定义任何必要的操作。

  2. 接下来，定义一个归纳谓词，断言原始嵌套类型中的所有映射或集合都格式良好。表明对原始类型的操作保持了格式良好。

  3. 通过定义 API 来构造嵌套归纳类型的适当接口，该 API 可根据需要证明格式良好的属性，并对用户隐藏它们。

Nested Inductive Types with Std.HashMap

此示例要求导入 Std.Data.HashMap.RawLemmas。 为了使代码更短，打开 Std 命名空间：

open Std

冒险游戏的地图可能由一系列通过通道连接的房间组成。 每个房间都有一个描述，每条通道都面向特定的方向。 这可以表示为递归结构。

(kernel) application type mismatch DHashMap.Raw.WF inner argument has type _nested.Std.DHashMap.Raw_3 but function has type (DHashMap.Raw String fun x => Maze) → Propstructure Maze where description : String passages : HashMap String Maze

这个定义被拒绝：

(kernel) application type mismatch
  DHashMap.Raw.WF inner
argument has type
  _nested.Std.DHashMap.Raw_3
but function has type
  (DHashMap.Raw String fun x => Maze) → Prop

要实现这项工作，需要将格式良好的谓词与结构分开。 第一步是重新定义不嵌入哈希映射不变量的类型：

structure RawMaze where description : String passages : Std.HashMap.Raw String RawMaze

最基本的原始迷宫没有通道：

def RawMaze.base (description : String) : RawMaze where description := description passages := ∅

可以使用 RawMaze.insert 将通向进一步迷宫的通道添加到原始迷宫中：

def RawMaze.insert (maze : RawMaze) (direction : String) (next : RawMaze) : RawMaze := { maze with passages := maze.passages.insert direction next }

第二步是为 RawMaze 定义一个格式良好的谓词，以确保每个包含的哈希映射都是格式良好的。 如果 passages 字段本身是良构的，并且其中包含的所有原始迷宫都是良构的，则原始迷宫是良构的。

inductive RawMaze.WF : RawMaze → Prop | mk {description passages} : (∀ (dir : String) v, passages[dir]? = some v → WF v) → passages.WF → WF { description, passages := passages }

基础迷宫是结构良好的，将通向结构良好的迷宫的通道插入到其他结构良好的迷宫中会产生结构良好的迷宫：

theorem RawMaze.base_wf (description : String) : RawMaze.WF (.base description) := description:String⊢ (base description).WF description:String⊢ ∀ (dir : String) (v : RawMaze), ∅[dir]? = some v → v.WFdescription:String⊢ ∅.WF description:String⊢ ∀ (dir : String) (v : RawMaze), ∅[dir]? = some v → v.WF description:Stringv:Stringh:RawMazeh':∅[v]? = some h⊢ h.WF All goals completed! 🐙 description:String⊢ ∅.WF All goals completed! 🐙 def RawMaze.insert_wf (maze : RawMaze) : WF maze → WF next → WF (maze.insert dir next) := next:RawMazedir:Stringmaze:RawMaze⊢ maze.WF → next.WF → (maze.insert dir next).WF next:RawMazedir:Stringmaze:RawMazedesc:Stringpassages:HashMap.Raw String RawMaze⊢ { description := desc, passages := passages }.WF → next.WF → ({ description := desc, passages := passages }.insert dir next).WF next:RawMazedir:Stringmaze:RawMazedesc:Stringpassages:HashMap.Raw String RawMazewfMore:∀ (dir : String) (v : RawMaze), passages[dir]? = some v → v.WFwfPassages:passages.WFwfNext:next.WF⊢ ({ description := desc, passages := passages }.insert dir next).WF next:RawMazedir:Stringmaze:RawMazedesc:Stringpassages:HashMap.Raw String RawMazewfMore:∀ (dir : String) (v : RawMaze), passages[dir]? = some v → v.WFwfPassages:passages.WFwfNext:next.WF⊢ ∀ (dir_1 : String) (v : RawMaze), ({ description := desc, passages := passages }.passages.insert dir next)[dir_1]? = some v → v.WFnext:RawMazedir:Stringmaze:RawMazedesc:Stringpassages:HashMap.Raw String RawMazewfMore:∀ (dir : String) (v : RawMaze), passages[dir]? = some v → v.WFwfPassages:passages.WFwfNext:next.WF⊢ ({ description := desc, passages := passages }.passages.insert dir next).WF next:RawMazedir:Stringmaze:RawMazedesc:Stringpassages:HashMap.Raw String RawMazewfMore:∀ (dir : String) (v : RawMaze), passages[dir]? = some v → v.WFwfPassages:passages.WFwfNext:next.WF⊢ ∀ (dir_1 : String) (v : RawMaze), ({ description := desc, passages := passages }.passages.insert dir next)[dir_1]? = some v → v.WF next:RawMazedir:Stringmaze:RawMazedesc:Stringpassages:HashMap.Raw String RawMazewfMore:∀ (dir : String) (v : RawMaze), passages[dir]? = some v → v.WFwfPassages:passages.WFwfNext:next.WFdir':Stringv:RawMaze⊢ ({ description := desc, passages := passages }.passages.insert dir next)[dir']? = some v → v.WF next:RawMazedir:Stringmaze:RawMazedesc:Stringpassages:HashMap.Raw String RawMazewfMore:∀ (dir : String) (v : RawMaze), passages[dir]? = some v → v.WFwfPassages:passages.WFwfNext:next.WFdir':Stringv:RawMaze⊢ (if (dir == dir') = true then some next else passages[dir']?) = some v → v.WF next:RawMazedir:Stringmaze:RawMazedesc:Stringpassages:HashMap.Raw String RawMazewfMore:∀ (dir : String) (v : RawMaze), passages[dir]? = some v → v.WFwfPassages:passages.WFwfNext:next.WFdir':Stringv:RawMazeh✝:(dir == dir') = true⊢ some next = some v → v.WFnext:RawMazedir:Stringmaze:RawMazedesc:Stringpassages:HashMap.Raw String RawMazewfMore:∀ (dir : String) (v : RawMaze), passages[dir]? = some v → v.WFwfPassages:passages.WFwfNext:next.WFdir':Stringv:RawMazeh✝:¬(dir == dir') = true⊢ passages[dir']? = some v → v.WF next:RawMazedir:Stringmaze:RawMazedesc:Stringpassages:HashMap.Raw String RawMazewfMore:∀ (dir : String) (v : RawMaze), passages[dir]? = some v → v.WFwfPassages:passages.WFwfNext:next.WFdir':Stringv:RawMazeh✝:(dir == dir') = true⊢ some next = some v → v.WFnext:RawMazedir:Stringmaze:RawMazedesc:Stringpassages:HashMap.Raw String RawMazewfMore:∀ (dir : String) (v : RawMaze), passages[dir]? = some v → v.WFwfPassages:passages.WFwfNext:next.WFdir':Stringv:RawMazeh✝:¬(dir == dir') = true⊢ passages[dir']? = some v → v.WF next:RawMazedir:Stringmaze:RawMazedesc:Stringpassages:HashMap.Raw String RawMazewfMore:∀ (dir : String) (v : RawMaze), passages[dir]? = some v → v.WFwfPassages:passages.WFwfNext:next.WFdir':Stringv:RawMazeh✝:¬(dir == dir') = truea✝:passages[dir']? = some v⊢ v.WF next:RawMazedir:Stringmaze:RawMazedesc:Stringpassages:HashMap.Raw String RawMazewfMore:∀ (dir : String) (v : RawMaze), passages[dir]? = some v → v.WFwfPassages:passages.WFwfNext:next.WFdir':Stringv:RawMazeh✝:(dir == dir') = truea✝:some next = some v⊢ v.WFnext:RawMazedir:Stringmaze:RawMazedesc:Stringpassages:HashMap.Raw String RawMazewfMore:∀ (dir : String) (v : RawMaze), passages[dir]? = some v → v.WFwfPassages:passages.WFwfNext:next.WFdir':Stringv:RawMazeh✝:¬(dir == dir') = truea✝:passages[dir']? = some v⊢ v.WF All goals completed! 🐙 next:RawMazedir:Stringmaze:RawMazedesc:Stringpassages:HashMap.Raw String RawMazewfMore:∀ (dir : String) (v : RawMaze), passages[dir]? = some v → v.WFwfPassages:passages.WFwfNext:next.WF⊢ ({ description := desc, passages := passages }.passages.insert dir next).WF All goals completed! 🐙

最后，可以定义一个更友好的界面，使用户不必担心格式良好。 Maze 将 RawMaze 与其格式良好的证明捆绑在一起：

structure Maze where raw : RawMaze wf : raw.WF

base 和 insert 运算符负责格式良好的证明义务：

def Maze.base (description : String) : Maze where raw := .base description wf := description:String⊢ (RawMaze.base description).WF All goals completed! 🐙 def Maze.insert (maze : Maze) (dir : String) (next : Maze) : Maze where raw := maze.raw.insert dir next.raw wf := RawMaze.insert_wf maze.raw maze.wf next.wf

Maze API 的用户可以检查当前迷宫​​的描述或尝试前往新迷宫的方向：

def Maze.description (maze : Maze) : String := maze.raw.description def Maze.go? (maze : Maze) (dir : String) : Option Maze := match h : maze.raw.passages[dir]? with | none => none | some m' => Maze.mk m' <| maze:Mazedir:Stringm':RawMazeh:maze.raw.passages[dir]? = some m'⊢ m'.WF maze:Mazedir:Stringm':RawMazer:RawMazewf:r.WFh:{ raw := r, wf := wf }.raw.passages[dir]? = some m'⊢ m'.WF maze:Mazedir:Stringm':RawMazer:RawMazewf:r.WFdescription✝:Stringpassages✝:HashMap.Raw String RawMazewfAll:∀ (dir : String) (v : RawMaze), passages✝[dir]? = some v → v.WFa✝:passages✝.WFh:{ raw := { description := description✝, passages := passages✝ }, wf := ⋯ }.raw.passages[dir]? = some m'⊢ m'.WF maze:Mazedir:Stringm':RawMazer:RawMazewf:r.WFdescription✝:Stringpassages✝:HashMap.Raw String RawMazewfAll:∀ (dir : String) (v : RawMaze), passages✝[dir]? = some v → v.WFa✝:passages✝.WFh:{ raw := { description := description✝, passages := passages✝ }, wf := ⋯ }.raw.passages[dir]? = some m'⊢ passages✝[dir]? = some m' All goals completed! 🐙
Live ↪

20.19.1.3. 适合唯一性的运算符🔗

使用数据结构时应小心，以确保尽可能多的引用是唯一的，这使得 Lean 能够在幕后使用破坏性突变，同时保持纯函数式接口。 地图和集合库提供可用于维护引用唯一性的运算符。 特别是，在可能的情况下，应优先选择诸如 alter 或 modify 之类的操作，而不是显式检索值、修改值并重新插入值。 这些操作避免在修改期间创建对该值的第二个引用。

Modifying Values in Maps
open Std

函数 addAlias 用于跟踪某些数据集中字符串的别名。 添加别名的一种方法是首先查找现有别名，默认为空数组，然后插入新别名，最后将结果数组保存在映射中：

def addAlias (aliases : HashMap String (Array String)) (key value : String) : HashMap String (Array String) := let prior := aliases.getD key #[] aliases.insert key (prior.push value)

此实现的性能特征很差。 由于映射保留了对先前值的引用，因此必须复制而不是更改数组。 更好的实现在修改之前显式地从映射中删除先前的值：

def addAlias' (aliases : HashMap String (Array String)) (key value : String) : HashMap String (Array String) := let prior := aliases.getD key #[] let aliases := aliases.erase key aliases.insert key (prior.push value)

使用 HashMap.alter 效果更好。 它消除了显式删除并重新插入值的需要：

def addAlias'' (aliases : HashMap String (Array String)) (key value : String) : HashMap String (Array String) := aliases.alter key fun prior? => some ((prior?.getD #[]).push value)
Live ↪

20.19.2. 哈希映射🔗

本节中的声明应使用 import Std.HashMap 导入。

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

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.

20.19.2.1. 创建🔗

🔗def
Std.HashMap.emptyWithCapacity.{u, v} {α : Type u} {β : Type v} [BEq α]
  [Hashable α] (capacity : Nat := 8) : Std.HashMap α β
Std.HashMap.emptyWithCapacity.{u, v}
  {α : Type u} {β : Type v} [BEq α]
  [Hashable α] (capacity : Nat := 8) :
  Std.HashMap α β

Creates a new empty hash map. The optional parameter capacity can be supplied to presize the map so that it can hold the given number of mappings without reallocating. It is also possible to use the empty collection notations ∅ and {} to create an empty hash map with the default capacity.

20.19.2.2. 特性🔗

🔗def
Std.HashMap.size.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m : Std.HashMap α β) : Nat
Std.HashMap.size.{u, v} {α : Type u}
  {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α}
  (m : Std.HashMap α β) : Nat

The number of mappings present in the hash map

🔗def
Std.HashMap.isEmpty.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m : Std.HashMap α β) : Bool
Std.HashMap.isEmpty.{u, v} {α : Type u}
  {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α}
  (m : Std.HashMap α β) : Bool

Returns true if the hash map contains no mappings.

Note that if your BEq instance is not reflexive or your Hashable instance is not lawful, then it is possible that this function returns false even though is not possible to get anything out of the hash map.

🔗structure
Std.HashMap.Equiv.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m₁ m₂ : Std.HashMap α β) : Prop
Std.HashMap.Equiv.{u, v} {α : Type u}
  {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α}
  (m₁ m₂ : Std.HashMap α β) : Prop

Two hash maps are equivalent in the sense of Equiv iff all the keys and values are equal.

Constructor

Std.HashMap.Equiv.mk.{u, v}

Fields

inner : m₁.inner.Equiv m₂.inner

Internal implementation detail of the hash map

syntaxEquivalence

关系 HashMap.Equiv 也可以使用中缀运算符编写，其范围仅限于其命名空间：

term ::= ...
    | Two hash maps are equivalent in the sense of `Equiv` iff
all the keys and values are equal.
term ~m term

20.19.2.3. 查询🔗

🔗def
Std.HashMap.contains.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m : Std.HashMap α β) (a : α) : Bool
Std.HashMap.contains.{u, v} {α : Type u}
  {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m : Std.HashMap α β)
  (a : α) : Bool

Returns true if there is a mapping for the given key. There is also a Prop-valued version of this: a ∈ m is equivalent to m.contains a = true.

Observe that this is different behavior than for lists: for lists, ∈ uses = and contains uses == for comparisons, while for hash maps, both use ==.

🔗def
Std.HashMap.get.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m : Std.HashMap α β) (a : α) (h : a ∈ m) : β
Std.HashMap.get.{u, v} {α : Type u}
  {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m : Std.HashMap α β)
  (a : α) (h : a ∈ m) : β

The notation m[a] or m[a]'h is preferred over calling this function directly.

Retrieves the mapping for the given key. Ensures that such a mapping exists by requiring a proof of a ∈ m.

🔗def
Std.HashMap.get!.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [Inhabited β] (m : Std.HashMap α β) (a : α) : β
Std.HashMap.get!.{u, v} {α : Type u}
  {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [Inhabited β]
  (m : Std.HashMap α β) (a : α) : β

The notation m[a]! is preferred over calling this function directly.

Tries to retrieve the mapping for the given key, panicking if no such mapping is present.

🔗def
Std.HashMap.get?.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m : Std.HashMap α β) (a : α) : Option β
Std.HashMap.get?.{u, v} {α : Type u}
  {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m : Std.HashMap α β)
  (a : α) : Option β

The notation m[a]? is preferred over calling this function directly.

Tries to retrieve the mapping for the given key, returning none if no such mapping is present.

🔗def
Std.HashMap.getD.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m : Std.HashMap α β) (a : α) (fallback : β) : β
Std.HashMap.getD.{u, v} {α : Type u}
  {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m : Std.HashMap α β)
  (a : α) (fallback : β) : β

Tries to retrieve the mapping for the given key, returning fallback if no such mapping is present.

🔗def
Std.HashMap.getKey.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m : Std.HashMap α β) (a : α) (h : a ∈ m) : α
Std.HashMap.getKey.{u, v} {α : Type u}
  {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m : Std.HashMap α β)
  (a : α) (h : a ∈ m) : α

Retrieves the key from the mapping that matches a. Ensures that such a mapping exists by requiring a proof of a ∈ m. The result is guaranteed to be pointer equal to the key in the map.

🔗def
Std.HashMap.getKey!.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [Inhabited α] (m : Std.HashMap α β) (a : α) : α
Std.HashMap.getKey!.{u, v} {α : Type u}
  {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [Inhabited α]
  (m : Std.HashMap α β) (a : α) : α

Checks if a mapping for the given key exists and returns the key if it does, otherwise panics. If no panic occurs the result is guaranteed to be pointer equal to the key in the map.

🔗def
Std.HashMap.getKey?.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m : Std.HashMap α β) (a : α) : Option α
Std.HashMap.getKey?.{u, v} {α : Type u}
  {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m : Std.HashMap α β)
  (a : α) : Option α

Checks if a mapping for the given key exists and returns the key if it does, otherwise none. The result in the some case is guaranteed to be pointer equal to the key in the map.

🔗def
Std.HashMap.getKeyD.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m : Std.HashMap α β) (a fallback : α) : α
Std.HashMap.getKeyD.{u, v} {α : Type u}
  {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m : Std.HashMap α β)
  (a fallback : α) : α

Checks if a mapping for the given key exists and returns the key if it does, otherwise fallback. If a mapping exists the result is guaranteed to be pointer equal to the key in the map.

🔗def
Std.HashMap.keys.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m : Std.HashMap α β) : List α
Std.HashMap.keys.{u, v} {α : Type u}
  {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α}
  (m : Std.HashMap α β) : List α

Returns a list of all keys present in the hash map in some order.

🔗def
Std.HashMap.keysArray.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m : Std.HashMap α β) : Array α
Std.HashMap.keysArray.{u, v} {α : Type u}
  {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α}
  (m : Std.HashMap α β) : Array α

Returns an array of all keys present in the hash map in some order.

🔗def
Std.HashMap.values.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m : Std.HashMap α β) : List β
Std.HashMap.values.{u, v} {α : Type u}
  {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α}
  (m : Std.HashMap α β) : List β

Returns a list of all values present in the hash map in some order.

🔗def
Std.HashMap.valuesArray.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m : Std.HashMap α β) : Array β
Std.HashMap.valuesArray.{u, v}
  {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α}
  (m : Std.HashMap α β) : Array β

Returns an array of all values present in the hash map in some order.

20.19.2.4. 修改🔗

🔗def
Std.HashMap.alter.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m : Std.HashMap α β) (a : α)
  (f : Option β → Option β) : Std.HashMap α β
Std.HashMap.alter.{u, v} {α : Type u}
  {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m : Std.HashMap α β)
  (a : α) (f : Option β → Option β) :
  Std.HashMap α β

Modifies in place the value associated with a given key, allowing creating new values and deleting values via an Option valued replacement function.

This function ensures that the value is used linearly.

🔗def
Std.HashMap.modify.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m : Std.HashMap α β) (a : α) (f : β → β) :
  Std.HashMap α β
Std.HashMap.modify.{u, v} {α : Type u}
  {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m : Std.HashMap α β)
  (a : α) (f : β → β) : Std.HashMap α β

Modifies in place the value associated with a given key.

This function ensures that the value is used linearly.

🔗def
Std.HashMap.containsThenInsert.{u, v} {α : Type u} {β : Type v}
  {x✝ : BEq α} {x✝¹ : Hashable α} (m : Std.HashMap α β) (a : α)
  (b : β) : Bool × Std.HashMap α β
Std.HashMap.containsThenInsert.{u, v}
  {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m : Std.HashMap α β)
  (a : α) (b : β) : Bool × Std.HashMap α β

Checks whether a key is present in a map, and unconditionally inserts a value for the key.

Equivalent to (but potentially faster than) calling contains followed by insert.

🔗def
Std.HashMap.containsThenInsertIfNew.{u, v} {α : Type u} {β : Type v}
  {x✝ : BEq α} {x✝¹ : Hashable α} (m : Std.HashMap α β) (a : α)
  (b : β) : Bool × Std.HashMap α β
Std.HashMap.containsThenInsertIfNew.{u, v}
  {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m : Std.HashMap α β)
  (a : α) (b : β) : Bool × Std.HashMap α β

Checks whether a key is present in a map and inserts a value for the key if it was not found.

If the returned Bool is true, then the returned map is unaltered. If the Bool is false, then the returned map has a new value inserted.

Equivalent to (but potentially faster than) calling contains followed by insertIfNew.

🔗def
Std.HashMap.erase.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m : Std.HashMap α β) (a : α) : Std.HashMap α β
Std.HashMap.erase.{u, v} {α : Type u}
  {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m : Std.HashMap α β)
  (a : α) : Std.HashMap α β

Removes the mapping for the given key if it exists.

🔗def
Std.HashMap.filter.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (f : α → β → Bool) (m : Std.HashMap α β) :
  Std.HashMap α β
Std.HashMap.filter.{u, v} {α : Type u}
  {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (f : α → β → Bool)
  (m : Std.HashMap α β) : Std.HashMap α β

Removes all mappings of the hash map for which the given function returns false.

🔗def
Std.HashMap.filterMap.{u, v, w} {α : Type u} {β : Type v} {γ : Type w}
  [BEq α] [Hashable α] (f : α → β → Option γ) (m : Std.HashMap α β) :
  Std.HashMap α γ
Std.HashMap.filterMap.{u, v, w}
  {α : Type u} {β : Type v} {γ : Type w}
  [BEq α] [Hashable α]
  (f : α → β → Option γ)
  (m : Std.HashMap α β) : Std.HashMap α γ

Updates the values of the hash map by applying the given function to all mappings, keeping only those mappings where the function returns some value.

🔗def
Std.HashMap.insert.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m : Std.HashMap α β) (a : α) (b : β) :
  Std.HashMap α β
Std.HashMap.insert.{u, v} {α : Type u}
  {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m : Std.HashMap α β)
  (a : α) (b : β) : Std.HashMap α β

Inserts the given mapping into the map. If there is already a mapping for the given key, then both key and value will be replaced.

Note: this replacement behavior is true for HashMap, DHashMap, HashMap.Raw and DHashMap.Raw. The insert function on HashSet and HashSet.Raw behaves differently: it will return the set unchanged if a matching key is already present.

🔗def
Std.HashMap.insertIfNew.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m : Std.HashMap α β) (a : α) (b : β) :
  Std.HashMap α β
Std.HashMap.insertIfNew.{u, v}
  {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m : Std.HashMap α β)
  (a : α) (b : β) : Std.HashMap α β

If there is no mapping for the given key, inserts the given mapping into the map. Otherwise, returns the map unaltered.

🔗def
Std.HashMap.getThenInsertIfNew?.{u, v} {α : Type u} {β : Type v}
  {x✝ : BEq α} {x✝¹ : Hashable α} (m : Std.HashMap α β) (a : α)
  (b : β) : Option β × Std.HashMap α β
Std.HashMap.getThenInsertIfNew?.{u, v}
  {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m : Std.HashMap α β)
  (a : α) (b : β) :
  Option β × Std.HashMap α β

Checks whether a key is present in a map, returning the associated value, and inserts a value for the key if it was not found.

If the returned value is some v, then the returned map is unaltered. If it is none, then the returned map has a new value inserted.

Equivalent to (but potentially faster than) calling get? followed by insertIfNew.

🔗def
Std.HashMap.insertMany.{u, v, w} {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} {ρ : Type w} [ForIn Id ρ (α × β)]
  (m : Std.HashMap α β) (l : ρ) : Std.HashMap α β
Std.HashMap.insertMany.{u, v, w}
  {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} {ρ : Type w}
  [ForIn Id ρ (α × β)]
  (m : Std.HashMap α β) (l : ρ) :
  Std.HashMap α β

Inserts multiple mappings into the hash map by iterating over the given collection and calling insert. If the same key appears multiple times, the last occurrence takes precedence.

Note: this precedence behavior is true for HashMap, DHashMap, HashMap.Raw and DHashMap.Raw. The insertMany function on HashSet and HashSet.Raw behaves differently: it will prefer the first appearance.

🔗def
Std.HashMap.insertManyIfNewUnit.{u, w} {α : Type u} {x✝ : BEq α}
  {x✝¹ : Hashable α} {ρ : Type w} [ForIn Id ρ α]
  (m : Std.HashMap α Unit) (l : ρ) : Std.HashMap α Unit
Std.HashMap.insertManyIfNewUnit.{u, w}
  {α : Type u} {x✝ : BEq α}
  {x✝¹ : Hashable α} {ρ : Type w}
  [ForIn Id ρ α] (m : Std.HashMap α Unit)
  (l : ρ) : Std.HashMap α Unit

Inserts multiple keys with the value () into the hash map by iterating over the given collection and calling insertIfNew. If the same key appears multiple times, the first occurrence takes precedence.

This is mainly useful to implement HashSet.insertMany, so if you are considering using this, HashSet or HashSet.Raw might be a better fit for you.

🔗def
Std.HashMap.partition.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (f : α → β → Bool) (m : Std.HashMap α β) :
  Std.HashMap α β × Std.HashMap α β
Std.HashMap.partition.{u, v} {α : Type u}
  {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (f : α → β → Bool)
  (m : Std.HashMap α β) :
  Std.HashMap α β × Std.HashMap α β

Partition a hash map into two hash map based on a predicate.

🔗def
Std.HashMap.union.{u, v} {α : Type u} {β : Type v} [BEq α] [Hashable α]
  (m₁ m₂ : Std.HashMap α β) : Std.HashMap α β
Std.HashMap.union.{u, v} {α : Type u}
  {β : Type v} [BEq α] [Hashable α]
  (m₁ m₂ : Std.HashMap α β) :
  Std.HashMap α β

Computes the union of the given hash maps. If a key appears in both maps, the entry contained in the second argument will appear in the result.

This function always merges the smaller map into the larger map, so the expected runtime is O(min(m₁.size, m₂.size)).

20.19.2.5. 迭代🔗

🔗def
Std.HashMap.iter.{u, v} {α : Type u} {β : Type v} [BEq α] [Hashable α]
  (m : Std.HashMap α β) : Std.Iter (α × β)
Std.HashMap.iter.{u, v} {α : Type u}
  {β : Type v} [BEq α] [Hashable α]
  (m : Std.HashMap α β) : Std.Iter (α × β)

Returns a finite iterator over the entries of a hash map. The iterator yields the elements of the map in order and then terminates.

Termination properties:

  • Finite instance: always

  • Productive instance: always

🔗def
Std.HashMap.keysIter.{u} {α β : Type u} [BEq α] [Hashable α]
  (m : Std.HashMap α β) : Std.Iter α
Std.HashMap.keysIter.{u} {α β : Type u}
  [BEq α] [Hashable α]
  (m : Std.HashMap α β) : Std.Iter α

Returns a finite iterator over the entries of a hash map. The iterator yields the elements of the map in order and then terminates.

Termination properties:

  • Finite instance: always

  • Productive instance: always

🔗def
Std.HashMap.valuesIter.{u} {α β : Type u} [BEq α] [Hashable α]
  (m : Std.HashMap α β) : Std.Iter β
Std.HashMap.valuesIter.{u} {α β : Type u}
  [BEq α] [Hashable α]
  (m : Std.HashMap α β) : Std.Iter β

Returns a finite iterator over the entries of a hash map. The iterator yields the elements of the map in order and then terminates.

Termination properties:

  • Finite instance: always

  • Productive instance: always

🔗def
Std.HashMap.map.{u, v, w} {α : Type u} {β : Type v} {γ : Type w} [BEq α]
  [Hashable α] (f : α → β → γ) (m : Std.HashMap α β) : Std.HashMap α γ
Std.HashMap.map.{u, v, w} {α : Type u}
  {β : Type v} {γ : Type w} [BEq α]
  [Hashable α] (f : α → β → γ)
  (m : Std.HashMap α β) : Std.HashMap α γ

Updates the values of the hash map by applying the given function to all mappings.

🔗def
Std.HashMap.fold.{u, v, w} {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} {γ : Type w} (f : γ → α → β → γ) (init : γ)
  (b : Std.HashMap α β) : γ
Std.HashMap.fold.{u, v, w} {α : Type u}
  {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} {γ : Type w}
  (f : γ → α → β → γ) (init : γ)
  (b : Std.HashMap α β) : γ

Folds the given function over the mappings in the hash map in some order.

🔗def
Std.HashMap.foldM.{u, v, w, w'} {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} {m : Type w → Type w'} [Monad m] {γ : Type w}
  (f : γ → α → β → m γ) (init : γ) (b : Std.HashMap α β) : m γ
Std.HashMap.foldM.{u, v, w, w'}
  {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α}
  {m : Type w → Type w'} [Monad m]
  {γ : Type w} (f : γ → α → β → m γ)
  (init : γ) (b : Std.HashMap α β) : m γ

Monadically computes a value by folding the given function over the mappings in the hash map in some order.

🔗def
Std.HashMap.forIn.{u, v, w, w'} {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} {m : Type w → Type w'} [Monad m] {γ : Type w}
  (f : α → β → γ → m (ForInStep γ)) (init : γ) (b : Std.HashMap α β) :
  m γ
Std.HashMap.forIn.{u, v, w, w'}
  {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α}
  {m : Type w → Type w'} [Monad m]
  {γ : Type w}
  (f : α → β → γ → m (ForInStep γ))
  (init : γ) (b : Std.HashMap α β) : m γ

Support for the for loop construct in do blocks.

🔗def
Std.HashMap.forM.{u, v, w, w'} {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} {m : Type w → Type w'} [Monad m]
  (f : α → β → m PUnit) (b : Std.HashMap α β) : m PUnit
Std.HashMap.forM.{u, v, w, w'}
  {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α}
  {m : Type w → Type w'} [Monad m]
  (f : α → β → m PUnit)
  (b : Std.HashMap α β) : m PUnit

Carries out a monadic action on each mapping in the hash map in some order.

20.19.2.6. 转换🔗

🔗def
Std.HashMap.ofList.{u, v} {α : Type u} {β : Type v} [BEq α] [Hashable α]
  (l : List (α × β)) : Std.HashMap α β
Std.HashMap.ofList.{u, v} {α : Type u}
  {β : Type v} [BEq α] [Hashable α]
  (l : List (α × β)) : Std.HashMap α β

Creates a hash map from a list of mappings. If the same key appears multiple times, the last occurrence takes precedence.

🔗def
Std.HashMap.toArray.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m : Std.HashMap α β) : Array (α × β)
Std.HashMap.toArray.{u, v} {α : Type u}
  {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α}
  (m : Std.HashMap α β) : Array (α × β)

Transforms the hash map into an array of mappings in some order.

🔗def
Std.HashMap.toList.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m : Std.HashMap α β) : List (α × β)
Std.HashMap.toList.{u, v} {α : Type u}
  {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α}
  (m : Std.HashMap α β) : List (α × β)

Transforms the hash map into a list of mappings in some order.

🔗def
Std.HashMap.unitOfArray.{u} {α : Type u} [BEq α] [Hashable α]
  (l : Array α) : Std.HashMap α Unit
Std.HashMap.unitOfArray.{u} {α : Type u}
  [BEq α] [Hashable α] (l : Array α) :
  Std.HashMap α Unit

Creates a hash map from an array of keys, associating the value () with each key.

This is mainly useful to implement HashSet.ofArray, so if you are considering using this, HashSet or HashSet.Raw might be a better fit for you.

🔗def
Std.HashMap.unitOfList.{u} {α : Type u} [BEq α] [Hashable α]
  (l : List α) : Std.HashMap α Unit
Std.HashMap.unitOfList.{u} {α : Type u}
  [BEq α] [Hashable α] (l : List α) :
  Std.HashMap α Unit

Creates a hash map from a list of keys, associating the value () with each key.

This is mainly useful to implement HashSet.ofList, so if you are considering using this, HashSet or HashSet.Raw might be a better fit for you.

20.19.2.7. 非捆绑变体🔗

未捆绑的地图将格式良好的证明与数据分开。 这在定义 嵌套归纳类型 时主要有用。 要使用这些变体，请导入模块 Std.HashMap.Raw 和 Std.HashMap.RawLemmas。

🔗structure
Std.HashMap.Raw.{u, v} (α : Type u) (β : Type v) : Type (max u v)
Std.HashMap.Raw.{u, v} (α : Type u)
  (β : Type v) : Type (max u v)

Hash maps without a bundled well-formedness invariant, suitable for use in nested inductive types. The well-formedness invariant is called Raw.WF. When in doubt, prefer HashMap over HashMap.Raw. Lemmas about the operations on Std.Data.HashMap.Raw are available in the module Std.Data.HashMap.RawLemmas.

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.

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

Constructor

Std.HashMap.Raw.mk.{u, v}

Fields

inner : Std.DHashMap.Raw α fun x => β

Internal implementation detail of the hash map

🔗structure
Std.HashMap.Raw.WF.{u, v} {α : Type u} {β : Type v} [BEq α] [Hashable α]
  (m : Std.HashMap.Raw α β) : Prop
Std.HashMap.Raw.WF.{u, v} {α : Type u}
  {β : Type v} [BEq α] [Hashable α]
  (m : Std.HashMap.Raw α β) : Prop

Well-formedness predicate for hash maps. Users of HashMap will not need to interact with this. Users of HashMap.Raw will need to provide proofs of WF to lemmas and should use lemmas WF.empty and WF.insert (which are always named exactly like the operations they are about) to show that map operations preserve well-formedness.

Constructor

Std.HashMap.Raw.WF.mk.{u, v}

Fields

out : m.inner.WF

Internal implementation detail of the hash map

20.19.3. 依赖哈希映射🔗

本节中的声明应使用 import Std.DHashMap 导入。

🔗structure
Std.DHashMap.{u, v} (α : Type u) (β : α → Type v) [BEq α] [Hashable α] :
  Type (max u v)
Std.DHashMap.{u, v} (α : Type u)
  (β : α → Type v) [BEq α] [Hashable α] :
  Type (max u v)

Dependent 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.DHashMap.Raw and Std.DHashMap.Raw.WF unbundle the invariant from the hash map. When in doubt, prefer DHashMap over DHashMap.Raw.

For a variant that is more convenient for use in proofs because of extensionalities, see Std.ExtDHashMap which is defined in the module Std.Data.ExtDHashMap.

20.19.3.1. 创建🔗

🔗def
Std.DHashMap.emptyWithCapacity.{u, v} {α : Type u} {β : α → Type v}
  [BEq α] [Hashable α] (capacity : Nat := 8) : Std.DHashMap α β
Std.DHashMap.emptyWithCapacity.{u, v}
  {α : Type u} {β : α → Type v} [BEq α]
  [Hashable α] (capacity : Nat := 8) :
  Std.DHashMap α β

Creates a new empty hash map. The optional parameter capacity can be supplied to presize the map so that it can hold the given number of mappings without reallocating. It is also possible to use the empty collection notations ∅ and {} to create an empty hash map with the default capacity.

20.19.3.2. 特性🔗

🔗def
Std.DHashMap.size.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m : Std.DHashMap α β) : Nat
Std.DHashMap.size.{u, v} {α : Type u}
  {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α}
  (m : Std.DHashMap α β) : Nat

The number of mappings present in the hash map

🔗def
Std.DHashMap.isEmpty.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m : Std.DHashMap α β) : Bool
Std.DHashMap.isEmpty.{u, v} {α : Type u}
  {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α}
  (m : Std.DHashMap α β) : Bool

Returns true if the hash map contains no mappings.

Note that if your BEq instance is not reflexive or your Hashable instance is not lawful, then it is possible that this function returns false even though is not possible to get anything out of the hash map.

🔗structure
Std.DHashMap.Equiv.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m₁ m₂ : Std.DHashMap α β) : Prop
Std.DHashMap.Equiv.{u, v} {α : Type u}
  {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α}
  (m₁ m₂ : Std.DHashMap α β) : Prop

Two hash maps are equivalent in the sense of Equiv iff all the keys and values are equal.

Constructor

Std.DHashMap.Equiv.mk.{u, v}

Fields

inner : m₁.inner.Equiv m₂.inner

Internal implementation detail of the hash map

syntaxEquivalence

关系 DHashMap.Equiv 也可以使用中缀运算符编写，其范围仅限于其命名空间：

term ::= ...
    | Two hash maps are equivalent in the sense of `Equiv` iff
all the keys and values are equal.
term ~m term

20.19.3.3. 查询🔗

🔗def
Std.DHashMap.contains.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m : Std.DHashMap α β) (a : α) : Bool
Std.DHashMap.contains.{u, v} {α : Type u}
  {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α}
  (m : Std.DHashMap α β) (a : α) : Bool

Returns true if there is a mapping for the given key. There is also a Prop-valued version of this: a ∈ m is equivalent to m.contains a = true.

Observe that this is different behavior than for lists: for lists, ∈ uses = and contains uses == for comparisons, while for hash maps, both use ==.

🔗def
Std.DHashMap.get.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [LawfulBEq α] (m : Std.DHashMap α β) (a : α)
  (h : a ∈ m) : β a
Std.DHashMap.get.{u, v} {α : Type u}
  {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [LawfulBEq α]
  (m : Std.DHashMap α β) (a : α)
  (h : a ∈ m) : β a

Retrieves the mapping for the given key. Ensures that such a mapping exists by requiring a proof of a ∈ m.

Uses the LawfulBEq instance to cast the retrieved value to the correct type.

🔗def
Std.DHashMap.get!.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [LawfulBEq α] (m : Std.DHashMap α β) (a : α)
  [Inhabited (β a)] : β a
Std.DHashMap.get!.{u, v} {α : Type u}
  {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [LawfulBEq α]
  (m : Std.DHashMap α β) (a : α)
  [Inhabited (β a)] : β a

Tries to retrieve the mapping for the given key, panicking if no such mapping is present.

Uses the LawfulBEq instance to cast the retrieved value to the correct type.

🔗def
Std.DHashMap.get?.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [LawfulBEq α] (m : Std.DHashMap α β) (a : α) :
  Option (β a)
Std.DHashMap.get?.{u, v} {α : Type u}
  {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [LawfulBEq α]
  (m : Std.DHashMap α β) (a : α) :
  Option (β a)

Tries to retrieve the mapping for the given key, returning none if no such mapping is present.

Uses the LawfulBEq instance to cast the retrieved value to the correct type.

🔗def
Std.DHashMap.getD.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [LawfulBEq α] (m : Std.DHashMap α β) (a : α)
  (fallback : β a) : β a
Std.DHashMap.getD.{u, v} {α : Type u}
  {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [LawfulBEq α]
  (m : Std.DHashMap α β) (a : α)
  (fallback : β a) : β a

Tries to retrieve the mapping for the given key, returning fallback if no such mapping is present.

Uses the LawfulBEq instance to cast the retrieved value to the correct type.

🔗def
Std.DHashMap.getKey.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m : Std.DHashMap α β) (a : α) (h : a ∈ m) : α
Std.DHashMap.getKey.{u, v} {α : Type u}
  {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α}
  (m : Std.DHashMap α β) (a : α)
  (h : a ∈ m) : α

Retrieves the key from the mapping that matches a. Ensures that such a mapping exists by requiring a proof of a ∈ m. The result is guaranteed to be pointer equal to the key in the map.

🔗def
Std.DHashMap.getKey!.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [Inhabited α] (m : Std.DHashMap α β) (a : α) : α
Std.DHashMap.getKey!.{u, v} {α : Type u}
  {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [Inhabited α]
  (m : Std.DHashMap α β) (a : α) : α

Checks if a mapping for the given key exists and returns the key if it does, otherwise panics. If no panic occurs the result is guaranteed to be pointer equal to the key in the map.

🔗def
Std.DHashMap.getKey?.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m : Std.DHashMap α β) (a : α) : Option α
Std.DHashMap.getKey?.{u, v} {α : Type u}
  {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α}
  (m : Std.DHashMap α β) (a : α) :
  Option α

Checks if a mapping for the given key exists and returns the key if it does, otherwise none. The result in the some case is guaranteed to be pointer equal to the key in the map.

🔗def
Std.DHashMap.getKeyD.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m : Std.DHashMap α β) (a fallback : α) : α
Std.DHashMap.getKeyD.{u, v} {α : Type u}
  {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α}
  (m : Std.DHashMap α β)
  (a fallback : α) : α

Checks if a mapping for the given key exists and returns the key if it does, otherwise fallback. If a mapping exists the result is guaranteed to be pointer equal to the key in the map.

🔗def
Std.DHashMap.keys.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m : Std.DHashMap α β) : List α
Std.DHashMap.keys.{u, v} {α : Type u}
  {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α}
  (m : Std.DHashMap α β) : List α

Returns a list of all keys present in the hash map in some order.

🔗def
Std.DHashMap.keysArray.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m : Std.DHashMap α β) : Array α
Std.DHashMap.keysArray.{u, v} {α : Type u}
  {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α}
  (m : Std.DHashMap α β) : Array α

Returns an array of all keys present in the hash map in some order.

🔗def
Std.DHashMap.values.{u, v} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α}
  {β : Type v} (m : Std.DHashMap α fun x => β) : List β
Std.DHashMap.values.{u, v} {α : Type u}
  {x✝ : BEq α} {x✝¹ : Hashable α}
  {β : Type v}
  (m : Std.DHashMap α fun x => β) : List β

Returns a list of all values present in the hash map in some order.

🔗def
Std.DHashMap.valuesArray.{u, v} {α : Type u} {x✝ : BEq α}
  {x✝¹ : Hashable α} {β : Type v} (m : Std.DHashMap α fun x => β) :
  Array β
Std.DHashMap.valuesArray.{u, v}
  {α : Type u} {x✝ : BEq α}
  {x✝¹ : Hashable α} {β : Type v}
  (m : Std.DHashMap α fun x => β) :
  Array β

Returns an array of all values present in the hash map in some order.

20.19.3.4. 修改🔗

🔗def
Std.DHashMap.alter.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [LawfulBEq α] (m : Std.DHashMap α β) (a : α)
  (f : Option (β a) → Option (β a)) : Std.DHashMap α β
Std.DHashMap.alter.{u, v} {α : Type u}
  {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [LawfulBEq α]
  (m : Std.DHashMap α β) (a : α)
  (f : Option (β a) → Option (β a)) :
  Std.DHashMap α β

Modifies in place the value associated with a given key, allowing creating new values and deleting values via an Option valued replacement function.

This function ensures that the value is used linearly.

🔗def
Std.DHashMap.modify.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [LawfulBEq α] (m : Std.DHashMap α β) (a : α)
  (f : β a → β a) : Std.DHashMap α β
Std.DHashMap.modify.{u, v} {α : Type u}
  {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [LawfulBEq α]
  (m : Std.DHashMap α β) (a : α)
  (f : β a → β a) : Std.DHashMap α β

Modifies in place the value associated with a given key.

This function ensures that the value is used linearly.

🔗def
Std.DHashMap.containsThenInsert.{u, v} {α : Type u} {β : α → Type v}
  {x✝ : BEq α} {x✝¹ : Hashable α} (m : Std.DHashMap α β) (a : α)
  (b : β a) : Bool × Std.DHashMap α β
Std.DHashMap.containsThenInsert.{u, v}
  {α : Type u} {β : α → Type v}
  {x✝ : BEq α} {x✝¹ : Hashable α}
  (m : Std.DHashMap α β) (a : α)
  (b : β a) : Bool × Std.DHashMap α β

Checks whether a key is present in a map, and unconditionally inserts a value for the key.

Equivalent to (but potentially faster than) calling contains followed by insert.

🔗def
Std.DHashMap.containsThenInsertIfNew.{u, v} {α : Type u}
  {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α}
  (m : Std.DHashMap α β) (a : α) (b : β a) : Bool × Std.DHashMap α β
Std.DHashMap.containsThenInsertIfNew.{u,
    v}
  {α : Type u} {β : α → Type v}
  {x✝ : BEq α} {x✝¹ : Hashable α}
  (m : Std.DHashMap α β) (a : α)
  (b : β a) : Bool × Std.DHashMap α β

Checks whether a key is present in a map and inserts a value for the key if it was not found.

If the returned Bool is true, then the returned map is unaltered. If the Bool is false, then the returned map has a new value inserted.

Equivalent to (but potentially faster than) calling contains followed by insertIfNew.

🔗def
Std.DHashMap.erase.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m : Std.DHashMap α β) (a : α) : Std.DHashMap α β
Std.DHashMap.erase.{u, v} {α : Type u}
  {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α}
  (m : Std.DHashMap α β) (a : α) :
  Std.DHashMap α β

Removes the mapping for the given key if it exists.

🔗def
Std.DHashMap.filter.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (f : (a : α) → β a → Bool) (m : Std.DHashMap α β) :
  Std.DHashMap α β
Std.DHashMap.filter.{u, v} {α : Type u}
  {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α}
  (f : (a : α) → β a → Bool)
  (m : Std.DHashMap α β) :
  Std.DHashMap α β

Removes all mappings of the hash map for which the given function returns false.

🔗def
Std.DHashMap.filterMap.{u, v, w} {α : Type u} {β : α → Type v}
  {δ : α → Type w} [BEq α] [Hashable α]
  (f : (a : α) → β a → Option (δ a)) (m : Std.DHashMap α β) :
  Std.DHashMap α δ
Std.DHashMap.filterMap.{u, v, w}
  {α : Type u} {β : α → Type v}
  {δ : α → Type w} [BEq α] [Hashable α]
  (f : (a : α) → β a → Option (δ a))
  (m : Std.DHashMap α β) :
  Std.DHashMap α δ

Updates the values of the hash map by applying the given function to all mappings, keeping only those mappings where the function returns some value.

🔗def
Std.DHashMap.insert.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m : Std.DHashMap α β) (a : α) (b : β a) :
  Std.DHashMap α β
Std.DHashMap.insert.{u, v} {α : Type u}
  {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α}
  (m : Std.DHashMap α β) (a : α)
  (b : β a) : Std.DHashMap α β

Inserts the given mapping into the map. If there is already a mapping for the given key, then both key and value will be replaced.

Note: this replacement behavior is true for HashMap, DHashMap, HashMap.Raw and DHashMap.Raw. The insert function on HashSet and HashSet.Raw behaves differently: it will return the set unchanged if a matching key is already present.

🔗def
Std.DHashMap.insertIfNew.{u, v} {α : Type u} {β : α → Type v}
  {x✝ : BEq α} {x✝¹ : Hashable α} (m : Std.DHashMap α β) (a : α)
  (b : β a) : Std.DHashMap α β
Std.DHashMap.insertIfNew.{u, v}
  {α : Type u} {β : α → Type v}
  {x✝ : BEq α} {x✝¹ : Hashable α}
  (m : Std.DHashMap α β) (a : α)
  (b : β a) : Std.DHashMap α β

If there is no mapping for the given key, inserts the given mapping into the map. Otherwise, returns the map unaltered.

🔗def
Std.DHashMap.getThenInsertIfNew?.{u, v} {α : Type u} {β : α → Type v}
  {x✝ : BEq α} {x✝¹ : Hashable α} [LawfulBEq α] (m : Std.DHashMap α β)
  (a : α) (b : β a) : Option (β a) × Std.DHashMap α β
Std.DHashMap.getThenInsertIfNew?.{u, v}
  {α : Type u} {β : α → Type v}
  {x✝ : BEq α} {x✝¹ : Hashable α}
  [LawfulBEq α] (m : Std.DHashMap α β)
  (a : α) (b : β a) :
  Option (β a) × Std.DHashMap α β

Checks whether a key is present in a map, returning the associated value, and inserts a value for the key if it was not found.

If the returned value is some v, then the returned map is unaltered. If it is none, then the returned map has a new value inserted.

Equivalent to (but potentially faster than) calling get? followed by insertIfNew.

Uses the LawfulBEq instance to cast the retrieved value to the correct type.

🔗def
Std.DHashMap.insertMany.{u, v, w} {α : Type u} {β : α → Type v}
  {x✝ : BEq α} {x✝¹ : Hashable α} {ρ : Type w}
  [ForIn Id ρ ((a : α) × β a)] (m : Std.DHashMap α β) (l : ρ) :
  Std.DHashMap α β
Std.DHashMap.insertMany.{u, v, w}
  {α : Type u} {β : α → Type v}
  {x✝ : BEq α} {x✝¹ : Hashable α}
  {ρ : Type w}
  [ForIn Id ρ ((a : α) × β a)]
  (m : Std.DHashMap α β) (l : ρ) :
  Std.DHashMap α β

Inserts multiple mappings into the hash map by iterating over the given collection and calling insert. If the same key appears multiple times, the last occurrence takes precedence.

Note: this precedence behavior is true for HashMap, DHashMap, HashMap.Raw and DHashMap.Raw. The insertMany function on HashSet and HashSet.Raw behaves differently: it will prefer the first appearance.

🔗def
Std.DHashMap.partition.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (f : (a : α) → β a → Bool) (m : Std.DHashMap α β) :
  Std.DHashMap α β × Std.DHashMap α β
Std.DHashMap.partition.{u, v} {α : Type u}
  {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α}
  (f : (a : α) → β a → Bool)
  (m : Std.DHashMap α β) :
  Std.DHashMap α β × Std.DHashMap α β

Partition a hash map into two hash map based on a predicate.

🔗def
Std.DHashMap.union.{u, v} {α : Type u} {β : α → Type v} [BEq α]
  [Hashable α] (m₁ m₂ : Std.DHashMap α β) : Std.DHashMap α β
Std.DHashMap.union.{u, v} {α : Type u}
  {β : α → Type v} [BEq α] [Hashable α]
  (m₁ m₂ : Std.DHashMap α β) :
  Std.DHashMap α β

Computes the union of the given hash maps. If a key appears in both maps, the entry contained in the second argument will appear in the result.

This function always merges the smaller map into the larger map, so the expected runtime is O(min(m₁.size, m₂.size)).

20.19.3.5. 迭代🔗

🔗def
Std.DHashMap.iter.{u, v} {α : Type u} {β : α → Type v} [BEq α]
  [Hashable α] (m : Std.DHashMap α β) : Std.Iter ((a : α) × β a)
Std.DHashMap.iter.{u, v} {α : Type u}
  {β : α → Type v} [BEq α] [Hashable α]
  (m : Std.DHashMap α β) :
  Std.Iter ((a : α) × β a)

Returns a finite iterator over the entries of a dependent hash map. The iterator yields the elements of the map in order and then terminates.

Termination properties:

  • Finite instance: always

  • Productive instance: always

🔗def
Std.DHashMap.keysIter.{u} {α : Type u} {β : α → Type u} [BEq α]
  [Hashable α] (m : Std.DHashMap α β) : Std.Iter α
Std.DHashMap.keysIter.{u} {α : Type u}
  {β : α → Type u} [BEq α] [Hashable α]
  (m : Std.DHashMap α β) : Std.Iter α

Returns a finite iterator over the keys of a dependent hash map. The iterator yields the keys in order and then terminates.

The key and value types must live in the same universe.

Termination properties:

  • Finite instance: always

  • Productive instance: always

🔗def
Std.DHashMap.valuesIter.{u} {α β : Type u} [BEq α] [Hashable α]
  (m : Std.DHashMap α fun x => β) : Std.Iter β
Std.DHashMap.valuesIter.{u} {α β : Type u}
  [BEq α] [Hashable α]
  (m : Std.DHashMap α fun x => β) :
  Std.Iter β

Returns a finite iterator over the values of a hash map. The iterator yields the values in order and then terminates.

The key and value types must live in the same universe.

Termination properties:

  • Finite instance: always

  • Productive instance: always

🔗def
Std.DHashMap.map.{u, v, w} {α : Type u} {β : α → Type v}
  {δ : α → Type w} [BEq α] [Hashable α] (f : (a : α) → β a → δ a)
  (m : Std.DHashMap α β) : Std.DHashMap α δ
Std.DHashMap.map.{u, v, w} {α : Type u}
  {β : α → Type v} {δ : α → Type w}
  [BEq α] [Hashable α]
  (f : (a : α) → β a → δ a)
  (m : Std.DHashMap α β) :
  Std.DHashMap α δ

Updates the values of the hash map by applying the given function to all mappings.

🔗def
Std.DHashMap.fold.{u, v, w} {α : Type u} {β : α → Type v} {δ : Type w}
  {x✝ : BEq α} {x✝¹ : Hashable α} (f : δ → (a : α) → β a → δ) (init : δ)
  (b : Std.DHashMap α β) : δ
Std.DHashMap.fold.{u, v, w} {α : Type u}
  {β : α → Type v} {δ : Type w}
  {x✝ : BEq α} {x✝¹ : Hashable α}
  (f : δ → (a : α) → β a → δ) (init : δ)
  (b : Std.DHashMap α β) : δ

Folds the given function over the mappings in the hash map in some order.

🔗def
Std.DHashMap.foldM.{u, v, w, w'} {α : Type u} {β : α → Type v}
  {δ : Type w} {m : Type w → Type w'} [Monad m] {x✝ : BEq α}
  {x✝¹ : Hashable α} (f : δ → (a : α) → β a → m δ) (init : δ)
  (b : Std.DHashMap α β) : m δ
Std.DHashMap.foldM.{u, v, w, w'}
  {α : Type u} {β : α → Type v}
  {δ : Type w} {m : Type w → Type w'}
  [Monad m] {x✝ : BEq α}
  {x✝¹ : Hashable α}
  (f : δ → (a : α) → β a → m δ) (init : δ)
  (b : Std.DHashMap α β) : m δ

Monadically computes a value by folding the given function over the mappings in the hash map in some order.

🔗def
Std.DHashMap.forIn.{u, v, w, w'} {α : Type u} {β : α → Type v}
  {δ : Type w} {m : Type w → Type w'} [Monad m] {x✝ : BEq α}
  {x✝¹ : Hashable α} (f : (a : α) → β a → δ → m (ForInStep δ))
  (init : δ) (b : Std.DHashMap α β) : m δ
Std.DHashMap.forIn.{u, v, w, w'}
  {α : Type u} {β : α → Type v}
  {δ : Type w} {m : Type w → Type w'}
  [Monad m] {x✝ : BEq α}
  {x✝¹ : Hashable α}
  (f :
    (a : α) → β a → δ → m (ForInStep δ))
  (init : δ) (b : Std.DHashMap α β) : m δ

Support for the for loop construct in do blocks.

🔗def
Std.DHashMap.forM.{u, v, w, w'} {α : Type u} {β : α → Type v}
  {m : Type w → Type w'} [Monad m] {x✝ : BEq α} {x✝¹ : Hashable α}
  (f : (a : α) → β a → m PUnit) (b : Std.DHashMap α β) : m PUnit
Std.DHashMap.forM.{u, v, w, w'}
  {α : Type u} {β : α → Type v}
  {m : Type w → Type w'} [Monad m]
  {x✝ : BEq α} {x✝¹ : Hashable α}
  (f : (a : α) → β a → m PUnit)
  (b : Std.DHashMap α β) : m PUnit

Carries out a monadic action on each mapping in the hash map in some order.

20.19.3.6. 转换🔗

🔗def
Std.DHashMap.ofList.{u, v} {α : Type u} {β : α → Type v} [BEq α]
  [Hashable α] (l : List ((a : α) × β a)) : Std.DHashMap α β
Std.DHashMap.ofList.{u, v} {α : Type u}
  {β : α → Type v} [BEq α] [Hashable α]
  (l : List ((a : α) × β a)) :
  Std.DHashMap α β

Creates a hash map from a list of mappings. If the same key appears multiple times, the last occurrence takes precedence.

🔗def
Std.DHashMap.toArray.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m : Std.DHashMap α β) : Array ((a : α) × β a)
Std.DHashMap.toArray.{u, v} {α : Type u}
  {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α}
  (m : Std.DHashMap α β) :
  Array ((a : α) × β a)

Transforms the hash map into an array of mappings in some order.

🔗def
Std.DHashMap.toList.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m : Std.DHashMap α β) : List ((a : α) × β a)
Std.DHashMap.toList.{u, v} {α : Type u}
  {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α}
  (m : Std.DHashMap α β) :
  List ((a : α) × β a)

Transforms the hash map into a list of mappings in some order.

20.19.3.7. 非捆绑变体🔗

未捆绑的地图将格式良好的证明与数据分开。 这在定义 嵌套归纳类型 时主要有用。 要使用这些变体，请导入模块 Std.DHashMap.Raw 和 Std.DHashMap.RawLemmas。

🔗structure
Std.DHashMap.Raw.{u, v} (α : Type u) (β : α → Type v) : Type (max u v)
Std.DHashMap.Raw.{u, v} (α : Type u)
  (β : α → Type v) : Type (max u v)

Dependent hash maps without a bundled well-formedness invariant, suitable for use in nested inductive types. The well-formedness invariant is called Raw.WF. When in doubt, prefer DHashMap over DHashMap.Raw. Lemmas about the operations on Std.Data.DHashMap.Raw are available in the module Std.Data.DHashMap.RawLemmas.

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

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

Constructor

Std.DHashMap.Raw.mk.{u, v}

Fields

size : Nat

The number of mappings present in the hash map

buckets : Array (Std.DHashMap.Internal.AssocList α β)

Internal implementation detail of the hash map

🔗inductive predicate
Std.DHashMap.Raw.WF.{u, v} {α : Type u} {β : α → Type v} [BEq α]
  [Hashable α] : Std.DHashMap.Raw α β → Prop
Std.DHashMap.Raw.WF.{u, v} {α : Type u}
  {β : α → Type v} [BEq α] [Hashable α] :
  Std.DHashMap.Raw α β → Prop

Well-formedness predicate for hash maps. Users of DHashMap will not need to interact with this. Users of DHashMap.Raw will need to provide proofs of WF to lemmas and should use lemmas like WF.empty and WF.insert (which are always named exactly like the operations they are about) to show that map operations preserve well-formedness. The constructors of this type are internal implementation details and should not be accessed by users.

Constructors

Std.DHashMap.Raw.WF.wf.{u, v} {α : Type u} {β : α → Type v}
  [BEq α] [Hashable α] {m : Std.DHashMap.Raw α β} :
  0 < m.buckets.size →
    (∀ [EquivBEq α] [LawfulHashable α],
        Std.DHashMap.Internal.Raw.WFImp m) →
      m.WF

Internal implementation detail of the hash map

Std.DHashMap.Raw.WF.emptyWithCapacity₀.{u, v} {α : Type u}
  {β : α → Type v} [BEq α] [Hashable α] {c : Nat} :
  (Std.DHashMap.Internal.Raw₀.emptyWithCapacity c).val.WF

Internal implementation detail of the hash map

Std.DHashMap.Raw.WF.insert₀.{u, v} {α : Type u}
  {β : α → Type v} [BEq α] [Hashable α]
  {m : Std.DHashMap.Raw α β} {h : 0 < m.buckets.size}
  {a : α} {b : β a} :
  m.WF →
    (Std.DHashMap.Internal.Raw₀.insert ⟨m, h⟩ a b).val.WF

Internal implementation detail of the hash map

Std.DHashMap.Raw.WF.containsThenInsert₀.{u, v} {α : Type u}
  {β : α → Type v} [BEq α] [Hashable α]
  {m : Std.DHashMap.Raw α β} {h : 0 < m.buckets.size}
  {a : α} {b : β a} :
  m.WF →
    (Std.DHashMap.Internal.Raw₀.containsThenInsert ⟨m, h⟩ a
            b).snd.val.WF

Internal implementation detail of the hash map

Std.DHashMap.Raw.WF.containsThenInsertIfNew₀.{u, v}
  {α : Type u} {β : α → Type v} [BEq α] [Hashable α]
  {m : Std.DHashMap.Raw α β} {h : 0 < m.buckets.size}
  {a : α} {b : β a} :
  m.WF →
    (Std.DHashMap.Internal.Raw₀.containsThenInsertIfNew
            ⟨m, h⟩ a b).snd.val.WF

Internal implementation detail of the hash map

Std.DHashMap.Raw.WF.erase₀.{u, v} {α : Type u}
  {β : α → Type v} [BEq α] [Hashable α]
  {m : Std.DHashMap.Raw α β} {h : 0 < m.buckets.size}
  {a : α} :
  m.WF → (Std.DHashMap.Internal.Raw₀.erase ⟨m, h⟩ a).val.WF

Internal implementation detail of the hash map

Std.DHashMap.Raw.WF.insertIfNew₀.{u, v} {α : Type u}
  {β : α → Type v} [BEq α] [Hashable α]
  {m : Std.DHashMap.Raw α β} {h : 0 < m.buckets.size}
  {a : α} {b : β a} :
  m.WF →
    (Std.DHashMap.Internal.Raw₀.insertIfNew ⟨m, h⟩ a
          b).val.WF

Internal implementation detail of the hash map

Std.DHashMap.Raw.WF.getThenInsertIfNew?₀.{u, v} {α : Type u}
  {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α]
  {m : Std.DHashMap.Raw α β} {h : 0 < m.buckets.size}
  {a : α} {b : β a} :
  m.WF →
    (Std.DHashMap.Internal.Raw₀.getThenInsertIfNew? ⟨m, h⟩ a
            b).snd.val.WF

Internal implementation detail of the hash map

Std.DHashMap.Raw.WF.filter₀.{u, v} {α : Type u}
  {β : α → Type v} [BEq α] [Hashable α]
  {m : Std.DHashMap.Raw α β} {h : 0 < m.buckets.size}
  {f : (a : α) → β a → Bool} :
  m.WF → (Std.DHashMap.Internal.Raw₀.filter f ⟨m, h⟩).val.WF

Internal implementation detail of the hash map

Std.DHashMap.Raw.WF.constGetThenInsertIfNew?₀.{u, v}
  {α : Type u} {β : Type v} [BEq α] [Hashable α]
  {m : Std.DHashMap.Raw α fun x => β}
  {h : 0 < m.buckets.size} {a : α} {b : β} :
  m.WF →
    (Std.DHashMap.Internal.Raw₀.Const.getThenInsertIfNew?
            ⟨m, h⟩ a b).snd.val.WF

Internal implementation detail of the hash map

Std.DHashMap.Raw.WF.modify₀.{u, v} {α : Type u}
  {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α]
  {m : Std.DHashMap.Raw α β} {h : 0 < m.buckets.size}
  {a : α} {f : β a → β a} :
  m.WF →
    (Std.DHashMap.Internal.Raw₀.modify ⟨m, h⟩ a f).val.WF

Internal implementation detail of the hash map

Std.DHashMap.Raw.WF.constModify₀.{u, v} {α : Type u}
  {β : Type v} [BEq α] [Hashable α]
  {m : Std.DHashMap.Raw α fun x => β}
  {h : 0 < m.buckets.size} {a : α} {f : β → β} :
  m.WF →
    (Std.DHashMap.Internal.Raw₀.Const.modify ⟨m, h⟩ a
          f).val.WF

Internal implementation detail of the hash map

Std.DHashMap.Raw.WF.alter₀.{u, v} {α : Type u}
  {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α]
  {m : Std.DHashMap.Raw α β} {h : 0 < m.buckets.size}
  {a : α} {f : Option (β a) → Option (β a)} :
  m.WF →
    (Std.DHashMap.Internal.Raw₀.alter ⟨m, h⟩ a f).val.WF

Internal implementation detail of the hash map

Std.DHashMap.Raw.WF.constAlter₀.{u, v} {α : Type u}
  {β : Type v} [BEq α] [Hashable α]
  {m : Std.DHashMap.Raw α fun x => β}
  {h : 0 < m.buckets.size} {a : α}
  {f : Option β → Option β} :
  m.WF →
    (Std.DHashMap.Internal.Raw₀.Const.alter ⟨m, h⟩ a
          f).val.WF

Internal implementation detail of the hash map

Std.DHashMap.Raw.WF.inter₀.{u, v} {α : Type u}
  {β : α → Type v} [BEq α] [Hashable α]
  {m₁ m₂ : Std.DHashMap.Raw α β} {h₁ : 0 < m₁.buckets.size}
  {h₂ : 0 < m₂.buckets.size} :
  m₁.WF →
    m₂.WF →
      (Std.DHashMap.Internal.Raw₀.inter ⟨m₁, h₁⟩
            ⟨m₂, h₂⟩).val.WF

Internal implementation detail of the hash map

20.19.4. 扩展哈希图🔗

本节中的声明应使用 import Std.ExtHashMap 导入。

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

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.

In contrast to regular hash maps, Std.ExtHashMap offers several extensionality lemmas and therefore has more lemmas about equality of hash maps. This however also makes it lose the ability to iterate freely over hash maps.

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.HashMap.Raw and Std.HashMap.Raw.WF unbundle the invariant from the hash map. When in doubt, prefer HashMap or ExtHashMap over HashMap.Raw.

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

20.19.4.1. 创建🔗

🔗def
Std.ExtHashMap.emptyWithCapacity.{u, v} {α : Type u} {β : Type v}
  [BEq α] [Hashable α] (capacity : Nat := 8) : Std.ExtHashMap α β
Std.ExtHashMap.emptyWithCapacity.{u, v}
  {α : Type u} {β : Type v} [BEq α]
  [Hashable α] (capacity : Nat := 8) :
  Std.ExtHashMap α β

Creates a new empty hash map. The optional parameter capacity can be supplied to presize the map so that it can hold the given number of mappings without reallocating. It is also possible to use the empty collection notations ∅ and {} to create an empty hash map with the default capacity.

20.19.4.2. 特性🔗

🔗def
Std.ExtHashMap.size.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]
  (m : Std.ExtHashMap α β) : Nat
Std.ExtHashMap.size.{u, v} {α : Type u}
  {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α]
  [LawfulHashable α]
  (m : Std.ExtHashMap α β) : Nat

The number of mappings present in the hash map

🔗def
Std.ExtHashMap.isEmpty.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]
  (m : Std.ExtHashMap α β) : Bool
Std.ExtHashMap.isEmpty.{u, v} {α : Type u}
  {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α]
  [LawfulHashable α]
  (m : Std.ExtHashMap α β) : Bool

Returns true if the hash map contains no mappings.

Note that if your BEq instance is not reflexive or your Hashable instance is not lawful, then it is possible that this function returns false even though is not possible to get anything out of the hash map.

20.19.4.3. 查询🔗

🔗def
Std.ExtHashMap.contains.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]
  (m : Std.ExtHashMap α β) (a : α) : Bool
Std.ExtHashMap.contains.{u, v}
  {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α]
  [LawfulHashable α]
  (m : Std.ExtHashMap α β) (a : α) : Bool

Returns true if there is a mapping for the given key. There is also a Prop-valued version of this: a ∈ m is equivalent to m.contains a = true.

Observe that this is different behavior than for lists: for lists, ∈ uses = and contains uses == for comparisons, while for hash maps, both use ==.

🔗def
Std.ExtHashMap.get.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]
  (m : Std.ExtHashMap α β) (a : α) (h : a ∈ m) : β
Std.ExtHashMap.get.{u, v} {α : Type u}
  {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α]
  [LawfulHashable α]
  (m : Std.ExtHashMap α β) (a : α)
  (h : a ∈ m) : β

The notation m[a] or m[a]'h is preferred over calling this function directly.

Retrieves the mapping for the given key. Ensures that such a mapping exists by requiring a proof of a ∈ m.

🔗def
Std.ExtHashMap.get!.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] [Inhabited β]
  (m : Std.ExtHashMap α β) (a : α) : β
Std.ExtHashMap.get!.{u, v} {α : Type u}
  {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α]
  [LawfulHashable α] [Inhabited β]
  (m : Std.ExtHashMap α β) (a : α) : β

The notation m[a]! is preferred over calling this function directly.

Tries to retrieve the mapping for the given key, panicking if no such mapping is present.

🔗def
Std.ExtHashMap.get?.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]
  (m : Std.ExtHashMap α β) (a : α) : Option β
Std.ExtHashMap.get?.{u, v} {α : Type u}
  {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α]
  [LawfulHashable α]
  (m : Std.ExtHashMap α β) (a : α) :
  Option β

The notation m[a]? is preferred over calling this function directly.

Tries to retrieve the mapping for the given key, returning none if no such mapping is present.

🔗def
Std.ExtHashMap.getD.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]
  (m : Std.ExtHashMap α β) (a : α) (fallback : β) : β
Std.ExtHashMap.getD.{u, v} {α : Type u}
  {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α]
  [LawfulHashable α]
  (m : Std.ExtHashMap α β) (a : α)
  (fallback : β) : β

Tries to retrieve the mapping for the given key, returning fallback if no such mapping is present.

🔗def
Std.ExtHashMap.getKey.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]
  (m : Std.ExtHashMap α β) (a : α) (h : a ∈ m) : α
Std.ExtHashMap.getKey.{u, v} {α : Type u}
  {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α]
  [LawfulHashable α]
  (m : Std.ExtHashMap α β) (a : α)
  (h : a ∈ m) : α

Retrieves the key from the mapping that matches a. Ensures that such a mapping exists by requiring a proof of a ∈ m. The result is guaranteed to be pointer equal to the key in the map.

🔗def
Std.ExtHashMap.getKey!.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] [Inhabited α]
  (m : Std.ExtHashMap α β) (a : α) : α
Std.ExtHashMap.getKey!.{u, v} {α : Type u}
  {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α]
  [LawfulHashable α] [Inhabited α]
  (m : Std.ExtHashMap α β) (a : α) : α

Checks if a mapping for the given key exists and returns the key if it does, otherwise panics. If no panic occurs the result is guaranteed to be pointer equal to the key in the map.

🔗def
Std.ExtHashMap.getKey?.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]
  (m : Std.ExtHashMap α β) (a : α) : Option α
Std.ExtHashMap.getKey?.{u, v} {α : Type u}
  {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α]
  [LawfulHashable α]
  (m : Std.ExtHashMap α β) (a : α) :
  Option α

Checks if a mapping for the given key exists and returns the key if it does, otherwise none. The result in the some case is guaranteed to be pointer equal to the key in the map.

🔗def
Std.ExtHashMap.getKeyD.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]
  (m : Std.ExtHashMap α β) (a fallback : α) : α
Std.ExtHashMap.getKeyD.{u, v} {α : Type u}
  {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α]
  [LawfulHashable α]
  (m : Std.ExtHashMap α β)
  (a fallback : α) : α

Checks if a mapping for the given key exists and returns the key if it does, otherwise fallback. If a mapping exists the result is guaranteed to be pointer equal to the key in the map.

20.19.4.4. 修改🔗

🔗def
Std.ExtHashMap.alter.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]
  (m : Std.ExtHashMap α β) (a : α) (f : Option β → Option β) :
  Std.ExtHashMap α β
Std.ExtHashMap.alter.{u, v} {α : Type u}
  {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α]
  [LawfulHashable α]
  (m : Std.ExtHashMap α β) (a : α)
  (f : Option β → Option β) :
  Std.ExtHashMap α β

Modifies in place the value associated with a given key, allowing creating new values and deleting values via an Option valued replacement function.

This function ensures that the value is used linearly.

🔗def
Std.ExtHashMap.modify.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]
  (m : Std.ExtHashMap α β) (a : α) (f : β → β) : Std.ExtHashMap α β
Std.ExtHashMap.modify.{u, v} {α : Type u}
  {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α]
  [LawfulHashable α]
  (m : Std.ExtHashMap α β) (a : α)
  (f : β → β) : Std.ExtHashMap α β

Modifies in place the value associated with a given key.

This function ensures that the value is used linearly.

🔗def
Std.ExtHashMap.containsThenInsert.{u, v} {α : Type u} {β : Type v}
  {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]
  (m : Std.ExtHashMap α β) (a : α) (b : β) : Bool × Std.ExtHashMap α β
Std.ExtHashMap.containsThenInsert.{u, v}
  {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α]
  [LawfulHashable α]
  (m : Std.ExtHashMap α β) (a : α)
  (b : β) : Bool × Std.ExtHashMap α β

Checks whether a key is present in a map, and unconditionally inserts a value for the key.

Equivalent to (but potentially faster than) calling contains followed by insert.

🔗def
Std.ExtHashMap.containsThenInsertIfNew.{u, v} {α : Type u} {β : Type v}
  {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]
  (m : Std.ExtHashMap α β) (a : α) (b : β) : Bool × Std.ExtHashMap α β
Std.ExtHashMap.containsThenInsertIfNew.{u,
    v}
  {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α]
  [LawfulHashable α]
  (m : Std.ExtHashMap α β) (a : α)
  (b : β) : Bool × Std.ExtHashMap α β

Checks whether a key is present in a map and inserts a value for the key if it was not found.

If the returned Bool is true, then the returned map is unaltered. If the Bool is false, then the returned map has a new value inserted.

Equivalent to (but potentially faster than) calling contains followed by insertIfNew.

🔗def
Std.ExtHashMap.erase.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]
  (m : Std.ExtHashMap α β) (a : α) : Std.ExtHashMap α β
Std.ExtHashMap.erase.{u, v} {α : Type u}
  {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α]
  [LawfulHashable α]
  (m : Std.ExtHashMap α β) (a : α) :
  Std.ExtHashMap α β

Removes the mapping for the given key if it exists.

🔗def
Std.ExtHashMap.filter.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] (f : α → β → Bool)
  (m : Std.ExtHashMap α β) : Std.ExtHashMap α β
Std.ExtHashMap.filter.{u, v} {α : Type u}
  {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α]
  [LawfulHashable α] (f : α → β → Bool)
  (m : Std.ExtHashMap α β) :
  Std.ExtHashMap α β

Removes all mappings of the hash map for which the given function returns false.

🔗def
Std.ExtHashMap.filterMap.{u, v, w} {α : Type u} {β : Type v}
  {γ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α]
  [LawfulHashable α] (f : α → β → Option γ) (m : Std.ExtHashMap α β) :
  Std.ExtHashMap α γ
Std.ExtHashMap.filterMap.{u, v, w}
  {α : Type u} {β : Type v} {γ : Type w}
  {x✝ : BEq α} {x✝¹ : Hashable α}
  [EquivBEq α] [LawfulHashable α]
  (f : α → β → Option γ)
  (m : Std.ExtHashMap α β) :
  Std.ExtHashMap α γ

Updates the values of the hash map by applying the given function to all mappings, keeping only those mappings where the function returns some value.

🔗def
Std.ExtHashMap.insert.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]
  (m : Std.ExtHashMap α β) (a : α) (b : β) : Std.ExtHashMap α β
Std.ExtHashMap.insert.{u, v} {α : Type u}
  {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α]
  [LawfulHashable α]
  (m : Std.ExtHashMap α β) (a : α)
  (b : β) : Std.ExtHashMap α β

Inserts the given mapping into the map. If there is already a mapping for the given key, then both key and value will be replaced.

Note: this replacement behavior is true for HashMap, DHashMap, HashMap.Raw and DHashMap.Raw. The insert function on HashSet and HashSet.Raw behaves differently: it will return the set unchanged if a matching key is already present.

🔗def
Std.ExtHashMap.insertIfNew.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]
  (m : Std.ExtHashMap α β) (a : α) (b : β) : Std.ExtHashMap α β
Std.ExtHashMap.insertIfNew.{u, v}
  {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α]
  [LawfulHashable α]
  (m : Std.ExtHashMap α β) (a : α)
  (b : β) : Std.ExtHashMap α β

If there is no mapping for the given key, inserts the given mapping into the map. Otherwise, returns the map unaltered.

🔗def
Std.ExtHashMap.getThenInsertIfNew?.{u, v} {α : Type u} {β : Type v}
  {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]
  (m : Std.ExtHashMap α β) (a : α) (b : β) :
  Option β × Std.ExtHashMap α β
Std.ExtHashMap.getThenInsertIfNew?.{u, v}
  {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α]
  [LawfulHashable α]
  (m : Std.ExtHashMap α β) (a : α)
  (b : β) : Option β × Std.ExtHashMap α β

Checks whether a key is present in a map, returning the associated value, and inserts a value for the key if it was not found.

If the returned value is some v, then the returned map is unaltered. If it is none, then the returned map has a new value inserted.

Equivalent to (but potentially faster than) calling get? followed by insertIfNew.

🔗def
Std.ExtHashMap.insertMany.{u, v, w} {α : Type u} {β : Type v}
  {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]
  {ρ : Type w} [ForIn Id ρ (α × β)] (m : Std.ExtHashMap α β) (l : ρ) :
  Std.ExtHashMap α β
Std.ExtHashMap.insertMany.{u, v, w}
  {α : Type u} {β : Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α]
  [LawfulHashable α] {ρ : Type w}
  [ForIn Id ρ (α × β)]
  (m : Std.ExtHashMap α β) (l : ρ) :
  Std.ExtHashMap α β

Inserts multiple mappings into the hash map by iterating over the given collection and calling insert. If the same key appears multiple times, the last occurrence takes precedence.

Note: this precedence behavior is true for HashMap, DHashMap, HashMap.Raw and DHashMap.Raw. The insertMany function on HashSet and HashSet.Raw behaves differently: it will prefer the first appearance.

🔗def
Std.ExtHashMap.insertManyIfNewUnit.{u, w} {α : Type u} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {ρ : Type w}
  [ForIn Id ρ α] (m : Std.ExtHashMap α Unit) (l : ρ) :
  Std.ExtHashMap α Unit
Std.ExtHashMap.insertManyIfNewUnit.{u, w}
  {α : Type u} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α]
  [LawfulHashable α] {ρ : Type w}
  [ForIn Id ρ α]
  (m : Std.ExtHashMap α Unit) (l : ρ) :
  Std.ExtHashMap α Unit

Inserts multiple keys with the value () into the hash map by iterating over the given collection and calling insertIfNew. If the same key appears multiple times, the first occurrence takes precedence.

This is mainly useful to implement HashSet.insertMany, so if you are considering using this, HashSet or HashSet.Raw might be a better fit for you.

20.19.4.5. 迭代🔗

🔗def
Std.ExtHashMap.map.{u, v, w} {α : Type u} {β : Type v} {γ : Type w}
  {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]
  (f : α → β → γ) (m : Std.ExtHashMap α β) : Std.ExtHashMap α γ
Std.ExtHashMap.map.{u, v, w} {α : Type u}
  {β : Type v} {γ : Type w} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α]
  [LawfulHashable α] (f : α → β → γ)
  (m : Std.ExtHashMap α β) :
  Std.ExtHashMap α γ

Updates the values of the hash map by applying the given function to all mappings.

20.19.4.6. 转换🔗

🔗def
Std.ExtHashMap.ofList.{u, v} {α : Type u} {β : Type v} [BEq α]
  [Hashable α] (l : List (α × β)) : Std.ExtHashMap α β
Std.ExtHashMap.ofList.{u, v} {α : Type u}
  {β : Type v} [BEq α] [Hashable α]
  (l : List (α × β)) : Std.ExtHashMap α β

Creates a hash map from a list of mappings. If the same key appears multiple times, the last occurrence takes precedence.

🔗def
Std.ExtHashMap.unitOfArray.{u} {α : Type u} [BEq α] [Hashable α]
  (l : Array α) : Std.ExtHashMap α Unit
Std.ExtHashMap.unitOfArray.{u}
  {α : Type u} [BEq α] [Hashable α]
  (l : Array α) : Std.ExtHashMap α Unit

Creates a hash map from an array of keys, associating the value () with each key.

This is mainly useful to implement HashSet.ofArray, so if you are considering using this, HashSet or HashSet.Raw might be a better fit for you.

🔗def
Std.ExtHashMap.unitOfList.{u} {α : Type u} [BEq α] [Hashable α]
  (l : List α) : Std.ExtHashMap α Unit
Std.ExtHashMap.unitOfList.{u} {α : Type u}
  [BEq α] [Hashable α] (l : List α) :
  Std.ExtHashMap α Unit

Creates a hash map from a list of keys, associating the value () with each key.

This is mainly useful to implement HashSet.ofList, so if you are considering using this, HashSet or HashSet.Raw might be a better fit for you.

20.19.5. 扩展依赖哈希图🔗

本节中的声明应使用 import Std.ExtDHashMap 导入。

🔗structure
Std.ExtDHashMap.{u, v} (α : Type u) (β : α → Type v) [BEq α]
  [Hashable α] : Type (max u v)
Std.ExtDHashMap.{u, v} (α : Type u)
  (β : α → Type v) [BEq α] [Hashable α] :
  Type (max u v)

Extensional dependent 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, == must be an equivalence relation and a == b must 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.

In contrast to regular dependent hash maps, Std.ExtDHashMap offers several extensionality lemmas and therefore has more lemmas about equality of hash maps. This however also makes it lose the ability to iterate freely over the hash map.

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.DHashMap.Raw and Std.DHashMap.Raw.WF unbundle the invariant from the hash map. When in doubt, prefer DHashMap over DHashMap.Raw.

20.19.5.1. 创建🔗

🔗def
Std.ExtDHashMap.emptyWithCapacity.{u, v} {α : Type u} {β : α → Type v}
  [BEq α] [Hashable α] (capacity : Nat := 8) : Std.ExtDHashMap α β
Std.ExtDHashMap.emptyWithCapacity.{u, v}
  {α : Type u} {β : α → Type v} [BEq α]
  [Hashable α] (capacity : Nat := 8) :
  Std.ExtDHashMap α β

Creates a new empty hash map. The optional parameter capacity can be supplied to presize the map so that it can hold the given number of mappings without reallocating. It is also possible to use the empty collection notations ∅ and {} to create an empty hash map with the default capacity.

20.19.5.2. 特性🔗

🔗def
Std.ExtDHashMap.size.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]
  (m : Std.ExtDHashMap α β) : Nat
Std.ExtDHashMap.size.{u, v} {α : Type u}
  {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α]
  [LawfulHashable α]
  (m : Std.ExtDHashMap α β) : Nat

The number of mappings present in the hash map

🔗def
Std.ExtDHashMap.isEmpty.{u, v} {α : Type u} {β : α → Type v}
  {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]
  (m : Std.ExtDHashMap α β) : Bool
Std.ExtDHashMap.isEmpty.{u, v}
  {α : Type u} {β : α → Type v}
  {x✝ : BEq α} {x✝¹ : Hashable α}
  [EquivBEq α] [LawfulHashable α]
  (m : Std.ExtDHashMap α β) : Bool

Returns true if the hash map contains no mappings.

Note that if your BEq instance is not reflexive or your Hashable instance is not lawful, then it is possible that this function returns false even though is not possible to get anything out of the hash map.

20.19.5.3. 查询🔗

🔗def
Std.ExtDHashMap.contains.{u, v} {α : Type u} {β : α → Type v}
  {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]
  (m : Std.ExtDHashMap α β) (a : α) : Bool
Std.ExtDHashMap.contains.{u, v}
  {α : Type u} {β : α → Type v}
  {x✝ : BEq α} {x✝¹ : Hashable α}
  [EquivBEq α] [LawfulHashable α]
  (m : Std.ExtDHashMap α β) (a : α) : Bool

Returns true if there is a mapping for the given key. There is also a Prop-valued version of this: a ∈ m is equivalent to m.contains a = true.

Observe that this is different behavior than for lists: for lists, ∈ uses = and contains uses == for comparisons, while for hash maps, both use ==.

🔗def
Std.ExtDHashMap.get.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [LawfulBEq α] (m : Std.ExtDHashMap α β) (a : α)
  (h : a ∈ m) : β a
Std.ExtDHashMap.get.{u, v} {α : Type u}
  {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [LawfulBEq α]
  (m : Std.ExtDHashMap α β) (a : α)
  (h : a ∈ m) : β a

Retrieves the mapping for the given key. Ensures that such a mapping exists by requiring a proof of a ∈ m.

Uses the LawfulBEq instance to cast the retrieved value to the correct type.

🔗def
Std.ExtDHashMap.get!.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [LawfulBEq α] (m : Std.ExtDHashMap α β) (a : α)
  [Inhabited (β a)] : β a
Std.ExtDHashMap.get!.{u, v} {α : Type u}
  {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [LawfulBEq α]
  (m : Std.ExtDHashMap α β) (a : α)
  [Inhabited (β a)] : β a

Tries to retrieve the mapping for the given key, panicking if no such mapping is present.

Uses the LawfulBEq instance to cast the retrieved value to the correct type.

🔗def
Std.ExtDHashMap.get?.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [LawfulBEq α] (m : Std.ExtDHashMap α β) (a : α) :
  Option (β a)
Std.ExtDHashMap.get?.{u, v} {α : Type u}
  {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [LawfulBEq α]
  (m : Std.ExtDHashMap α β) (a : α) :
  Option (β a)

Tries to retrieve the mapping for the given key, returning none if no such mapping is present.

Uses the LawfulBEq instance to cast the retrieved value to the correct type.

🔗def
Std.ExtDHashMap.getD.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [LawfulBEq α] (m : Std.ExtDHashMap α β) (a : α)
  (fallback : β a) : β a
Std.ExtDHashMap.getD.{u, v} {α : Type u}
  {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [LawfulBEq α]
  (m : Std.ExtDHashMap α β) (a : α)
  (fallback : β a) : β a

Tries to retrieve the mapping for the given key, returning fallback if no such mapping is present.

Uses the LawfulBEq instance to cast the retrieved value to the correct type.

🔗def
Std.ExtDHashMap.getKey.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]
  (m : Std.ExtDHashMap α β) (a : α) (h : a ∈ m) : α
Std.ExtDHashMap.getKey.{u, v} {α : Type u}
  {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α]
  [LawfulHashable α]
  (m : Std.ExtDHashMap α β) (a : α)
  (h : a ∈ m) : α

Retrieves the key from the mapping that matches a. Ensures that such a mapping exists by requiring a proof of a ∈ m. The result is guaranteed to be pointer equal to the key in the map.

🔗def
Std.ExtDHashMap.getKey!.{u, v} {α : Type u} {β : α → Type v}
  {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]
  [Inhabited α] (m : Std.ExtDHashMap α β) (a : α) : α
Std.ExtDHashMap.getKey!.{u, v}
  {α : Type u} {β : α → Type v}
  {x✝ : BEq α} {x✝¹ : Hashable α}
  [EquivBEq α] [LawfulHashable α]
  [Inhabited α] (m : Std.ExtDHashMap α β)
  (a : α) : α

Checks if a mapping for the given key exists and returns the key if it does, otherwise panics. If no panic occurs the result is guaranteed to be pointer equal to the key in the map.

🔗def
Std.ExtDHashMap.getKey?.{u, v} {α : Type u} {β : α → Type v}
  {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]
  (m : Std.ExtDHashMap α β) (a : α) : Option α
Std.ExtDHashMap.getKey?.{u, v}
  {α : Type u} {β : α → Type v}
  {x✝ : BEq α} {x✝¹ : Hashable α}
  [EquivBEq α] [LawfulHashable α]
  (m : Std.ExtDHashMap α β) (a : α) :
  Option α

Checks if a mapping for the given key exists and returns the key if it does, otherwise none. The result in the some case is guaranteed to be pointer equal to the key in the map.

🔗def
Std.ExtDHashMap.getKeyD.{u, v} {α : Type u} {β : α → Type v}
  {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]
  (m : Std.ExtDHashMap α β) (a fallback : α) : α
Std.ExtDHashMap.getKeyD.{u, v}
  {α : Type u} {β : α → Type v}
  {x✝ : BEq α} {x✝¹ : Hashable α}
  [EquivBEq α] [LawfulHashable α]
  (m : Std.ExtDHashMap α β)
  (a fallback : α) : α

Checks if a mapping for the given key exists and returns the key if it does, otherwise fallback. If a mapping exists the result is guaranteed to be pointer equal to the key in the map.

20.19.5.4. 修改🔗

🔗def
Std.ExtDHashMap.alter.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [LawfulBEq α] (m : Std.ExtDHashMap α β) (a : α)
  (f : Option (β a) → Option (β a)) : Std.ExtDHashMap α β
Std.ExtDHashMap.alter.{u, v} {α : Type u}
  {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [LawfulBEq α]
  (m : Std.ExtDHashMap α β) (a : α)
  (f : Option (β a) → Option (β a)) :
  Std.ExtDHashMap α β

Modifies in place the value associated with a given key, allowing creating new values and deleting values via an Option valued replacement function.

This function ensures that the value is used linearly.

🔗def
Std.ExtDHashMap.modify.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [LawfulBEq α] (m : Std.ExtDHashMap α β) (a : α)
  (f : β a → β a) : Std.ExtDHashMap α β
Std.ExtDHashMap.modify.{u, v} {α : Type u}
  {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [LawfulBEq α]
  (m : Std.ExtDHashMap α β) (a : α)
  (f : β a → β a) : Std.ExtDHashMap α β

Modifies in place the value associated with a given key.

This function ensures that the value is used linearly.

🔗def
Std.ExtDHashMap.containsThenInsert.{u, v} {α : Type u} {β : α → Type v}
  {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]
  (m : Std.ExtDHashMap α β) (a : α) (b : β a) :
  Bool × Std.ExtDHashMap α β
Std.ExtDHashMap.containsThenInsert.{u, v}
  {α : Type u} {β : α → Type v}
  {x✝ : BEq α} {x✝¹ : Hashable α}
  [EquivBEq α] [LawfulHashable α]
  (m : Std.ExtDHashMap α β) (a : α)
  (b : β a) : Bool × Std.ExtDHashMap α β

Checks whether a key is present in a map, and unconditionally inserts a value for the key.

Equivalent to (but potentially faster than) calling contains followed by insert.

🔗def
Std.ExtDHashMap.containsThenInsertIfNew.{u, v} {α : Type u}
  {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α]
  [LawfulHashable α] (m : Std.ExtDHashMap α β) (a : α) (b : β a) :
  Bool × Std.ExtDHashMap α β
Std.ExtDHashMap.containsThenInsertIfNew.{u,
    v}
  {α : Type u} {β : α → Type v}
  {x✝ : BEq α} {x✝¹ : Hashable α}
  [EquivBEq α] [LawfulHashable α]
  (m : Std.ExtDHashMap α β) (a : α)
  (b : β a) : Bool × Std.ExtDHashMap α β

Checks whether a key is present in a map and inserts a value for the key if it was not found.

If the returned Bool is true, then the returned map is unaltered. If the Bool is false, then the returned map has a new value inserted.

Equivalent to (but potentially faster than) calling contains followed by insertIfNew.

🔗def
Std.ExtDHashMap.erase.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]
  (m : Std.ExtDHashMap α β) (a : α) : Std.ExtDHashMap α β
Std.ExtDHashMap.erase.{u, v} {α : Type u}
  {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α]
  [LawfulHashable α]
  (m : Std.ExtDHashMap α β) (a : α) :
  Std.ExtDHashMap α β

Removes the mapping for the given key if it exists.

🔗def
Std.ExtDHashMap.filter.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]
  (f : (a : α) → β a → Bool) (m : Std.ExtDHashMap α β) :
  Std.ExtDHashMap α β
Std.ExtDHashMap.filter.{u, v} {α : Type u}
  {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α]
  [LawfulHashable α]
  (f : (a : α) → β a → Bool)
  (m : Std.ExtDHashMap α β) :
  Std.ExtDHashMap α β

Removes all mappings of the hash map for which the given function returns false.

🔗def
Std.ExtDHashMap.filterMap.{u, v, w} {α : Type u} {β : α → Type v}
  {γ : α → Type w} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α]
  [LawfulHashable α] (f : (a : α) → β a → Option (γ a))
  (m : Std.ExtDHashMap α β) : Std.ExtDHashMap α γ
Std.ExtDHashMap.filterMap.{u, v, w}
  {α : Type u} {β : α → Type v}
  {γ : α → Type w} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α]
  [LawfulHashable α]
  (f : (a : α) → β a → Option (γ a))
  (m : Std.ExtDHashMap α β) :
  Std.ExtDHashMap α γ

Updates the values of the hash map by applying the given function to all mappings, keeping only those mappings where the function returns some value.

🔗def
Std.ExtDHashMap.insert.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]
  (m : Std.ExtDHashMap α β) (a : α) (b : β a) : Std.ExtDHashMap α β
Std.ExtDHashMap.insert.{u, v} {α : Type u}
  {β : α → Type v} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α]
  [LawfulHashable α]
  (m : Std.ExtDHashMap α β) (a : α)
  (b : β a) : Std.ExtDHashMap α β

Inserts the given mapping into the map. If there is already a mapping for the given key, then both key and value will be replaced.

Note: this replacement behavior is true for HashMap, DHashMap, HashMap.Raw and DHashMap.Raw. The insert function on HashSet and HashSet.Raw behaves differently: it will return the set unchanged if a matching key is already present.

🔗def
Std.ExtDHashMap.insertIfNew.{u, v} {α : Type u} {β : α → Type v}
  {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]
  (m : Std.ExtDHashMap α β) (a : α) (b : β a) : Std.ExtDHashMap α β
Std.ExtDHashMap.insertIfNew.{u, v}
  {α : Type u} {β : α → Type v}
  {x✝ : BEq α} {x✝¹ : Hashable α}
  [EquivBEq α] [LawfulHashable α]
  (m : Std.ExtDHashMap α β) (a : α)
  (b : β a) : Std.ExtDHashMap α β

If there is no mapping for the given key, inserts the given mapping into the map. Otherwise, returns the map unaltered.

🔗def
Std.ExtDHashMap.getThenInsertIfNew?.{u, v} {α : Type u} {β : α → Type v}
  {x✝ : BEq α} {x✝¹ : Hashable α} [LawfulBEq α]
  (m : Std.ExtDHashMap α β) (a : α) (b : β a) :
  Option (β a) × Std.ExtDHashMap α β
Std.ExtDHashMap.getThenInsertIfNew?.{u, v}
  {α : Type u} {β : α → Type v}
  {x✝ : BEq α} {x✝¹ : Hashable α}
  [LawfulBEq α] (m : Std.ExtDHashMap α β)
  (a : α) (b : β a) :
  Option (β a) × Std.ExtDHashMap α β

Checks whether a key is present in a map, returning the associated value, and inserts a value for the key if it was not found.

If the returned value is some v, then the returned map is unaltered. If it is none, then the returned map has a new value inserted.

Equivalent to (but potentially faster than) calling get? followed by insertIfNew.

Uses the LawfulBEq instance to cast the retrieved value to the correct type.

🔗def
Std.ExtDHashMap.insertMany.{u, v, w} {α : Type u} {β : α → Type v}
  {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]
  {ρ : Type w} [ForIn Id ρ ((a : α) × β a)] (m : Std.ExtDHashMap α β)
  (l : ρ) : Std.ExtDHashMap α β
Std.ExtDHashMap.insertMany.{u, v, w}
  {α : Type u} {β : α → Type v}
  {x✝ : BEq α} {x✝¹ : Hashable α}
  [EquivBEq α] [LawfulHashable α]
  {ρ : Type w}
  [ForIn Id ρ ((a : α) × β a)]
  (m : Std.ExtDHashMap α β) (l : ρ) :
  Std.ExtDHashMap α β

Inserts multiple mappings into the hash map by iterating over the given collection and calling insert. If the same key appears multiple times, the last occurrence takes precedence.

Note: this precedence behavior is true for HashMap, DHashMap, HashMap.Raw and DHashMap.Raw. The insertMany function on HashSet and HashSet.Raw behaves differently: it will prefer the first appearance.

20.19.5.5. 迭代🔗

🔗def
Std.ExtDHashMap.map.{u, v, w} {α : Type u} {β : α → Type v}
  {γ : α → Type w} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α]
  [LawfulHashable α] (f : (a : α) → β a → γ a)
  (m : Std.ExtDHashMap α β) : Std.ExtDHashMap α γ
Std.ExtDHashMap.map.{u, v, w} {α : Type u}
  {β : α → Type v} {γ : α → Type w}
  {x✝ : BEq α} {x✝¹ : Hashable α}
  [EquivBEq α] [LawfulHashable α]
  (f : (a : α) → β a → γ a)
  (m : Std.ExtDHashMap α β) :
  Std.ExtDHashMap α γ

Updates the values of the hash map by applying the given function to all mappings.

20.19.5.6. 转换🔗

🔗def
Std.ExtDHashMap.ofList.{u, v} {α : Type u} {β : α → Type v} [BEq α]
  [Hashable α] (l : List ((a : α) × β a)) : Std.ExtDHashMap α β
Std.ExtDHashMap.ofList.{u, v} {α : Type u}
  {β : α → Type v} [BEq α] [Hashable α]
  (l : List ((a : α) × β a)) :
  Std.ExtDHashMap α β

Creates a hash map from a list of mappings. If the same key appears multiple times, the last occurrence takes precedence.

20.19.6. 哈希集🔗

🔗structure
Std.HashSet.{u} (α : Type u) [BEq α] [Hashable α] : Type u
Std.HashSet.{u} (α : Type u) [BEq α]
  [Hashable α] : Type u

Hash sets.

This is a simple separate-chaining hash table. The data of the hash set consists of a cached size and an array of buckets, where each bucket is a linked list of keys. The number of buckets is always a power of two. The hash set 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 set is used linearly to avoid expensive copies.

The hash set uses == (provided by the BEq typeclass) to compare elements 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 sets contain a bundled well-formedness invariant, which means that they cannot be used in nested inductive types. For these use cases, Std.Data.HashSet.Raw and Std.Data.HashSet.Raw.WF unbundle the invariant from the hash set. When in doubt, prefer HashSet over HashSet.Raw.

Constructor

Std.HashSet.mk.{u}

Fields

inner : Std.HashMap α Unit

Internal implementation detail of the hash set.

20.19.6.1. 创建🔗

🔗def
Std.HashSet.emptyWithCapacity.{u} {α : Type u} [BEq α] [Hashable α]
  (capacity : Nat := 8) : Std.HashSet α
Std.HashSet.emptyWithCapacity.{u}
  {α : Type u} [BEq α] [Hashable α]
  (capacity : Nat := 8) : Std.HashSet α

Creates a new empty hash set. The optional parameter capacity can be supplied to presize the set so that it can hold the given number of elements without reallocating. It is also possible to use the empty collection notations ∅ and {} to create an empty hash set with the default capacity.

20.19.6.2. 特性🔗

🔗def
Std.HashSet.isEmpty.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α}
  (m : Std.HashSet α) : Bool
Std.HashSet.isEmpty.{u} {α : Type u}
  {x✝ : BEq α} {x✝¹ : Hashable α}
  (m : Std.HashSet α) : Bool

Returns true if the hash set contains no elements.

Note that if your BEq instance is not reflexive or your Hashable instance is not lawful, then it is possible that this function returns false even though m.contains a = false for all a.

🔗def
Std.HashSet.size.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α}
  (m : Std.HashSet α) : Nat
Std.HashSet.size.{u} {α : Type u}
  {x✝ : BEq α} {x✝¹ : Hashable α}
  (m : Std.HashSet α) : Nat

The number of elements present in the set

🔗structure
Std.HashSet.Equiv.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α}
  (m₁ m₂ : Std.HashSet α) : Prop
Std.HashSet.Equiv.{u} {α : Type u}
  {x✝ : BEq α} {x✝¹ : Hashable α}
  (m₁ m₂ : Std.HashSet α) : Prop

Two hash sets are equivalent in the sense of Equiv iff all their values are equal.

Constructor

Std.HashSet.Equiv.mk.{u}

Fields

inner : m₁.inner.Equiv m₂.inner

Internal implementation detail of the hash map

syntaxEquivalence

关系 HashSet.Equiv 也可以使用中缀运算符编写，其范围仅限于其命名空间：

term ::= ...
    | Two hash maps are equivalent in the sense of `Equiv` iff
all the keys and values are equal.
term ~m term

20.19.6.3. 查询🔗

🔗def
Std.HashSet.contains.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α}
  (m : Std.HashSet α) (a : α) : Bool
Std.HashSet.contains.{u} {α : Type u}
  {x✝ : BEq α} {x✝¹ : Hashable α}
  (m : Std.HashSet α) (a : α) : Bool

Returns true if the given key is present in the set. There is also a Prop-valued version of this: a ∈ m is equivalent to m.contains a = true.

Observe that this is different behavior than for lists: for lists, ∈ uses = and contains use == for comparisons, while for hash sets, both use ==.

🔗def
Std.HashSet.get.{u} {α : Type u} [BEq α] [Hashable α]
  (m : Std.HashSet α) (a : α) (h : a ∈ m) : α
Std.HashSet.get.{u} {α : Type u} [BEq α]
  [Hashable α] (m : Std.HashSet α) (a : α)
  (h : a ∈ m) : α

Retrieves the key from the set that matches a. Ensures that such a key exists by requiring a proof of a ∈ m. The result is guaranteed to be pointer equal to the key in the set.

🔗def
Std.HashSet.get!.{u} {α : Type u} [BEq α] [Hashable α] [Inhabited α]
  (m : Std.HashSet α) (a : α) : α
Std.HashSet.get!.{u} {α : Type u} [BEq α]
  [Hashable α] [Inhabited α]
  (m : Std.HashSet α) (a : α) : α

Checks if given key is contained and returns the key if it is, otherwise panics. If no panic occurs the result is guaranteed to be pointer equal to the key in the set.

🔗def
Std.HashSet.get?.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α}
  (m : Std.HashSet α) (a : α) : Option α
Std.HashSet.get?.{u} {α : Type u}
  {x✝ : BEq α} {x✝¹ : Hashable α}
  (m : Std.HashSet α) (a : α) : Option α

Checks if given key is contained and returns the key if it is, otherwise none. The result in the some case is guaranteed to be pointer equal to the key in the set.

🔗def
Std.HashSet.getD.{u} {α : Type u} [BEq α] [Hashable α]
  (m : Std.HashSet α) (a fallback : α) : α
Std.HashSet.getD.{u} {α : Type u} [BEq α]
  [Hashable α] (m : Std.HashSet α)
  (a fallback : α) : α

Checks if given key is contained and returns the key if it is, otherwise fallback. If they key is contained the result is guaranteed to be pointer equal to the key in the set.

20.19.6.4. 修改🔗

🔗def
Std.HashSet.insert.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α}
  (m : Std.HashSet α) (a : α) : Std.HashSet α
Std.HashSet.insert.{u} {α : Type u}
  {x✝ : BEq α} {x✝¹ : Hashable α}
  (m : Std.HashSet α) (a : α) :
  Std.HashSet α

Inserts the given element into the set. If the hash set already contains an element that is equal (with regard to ==) to the given element, then the hash set is returned unchanged.

Note: this non-replacement behavior is true for HashSet and HashSet.Raw. The insert function on HashMap, DHashMap, HashMap.Raw and DHashMap.Raw behaves differently: it will overwrite an existing mapping.

🔗def
Std.HashSet.insertMany.{u, v} {α : Type u} {x✝ : BEq α}
  {x✝¹ : Hashable α} {ρ : Type v} [ForIn Id ρ α] (m : Std.HashSet α)
  (l : ρ) : Std.HashSet α
Std.HashSet.insertMany.{u, v} {α : Type u}
  {x✝ : BEq α} {x✝¹ : Hashable α}
  {ρ : Type v} [ForIn Id ρ α]
  (m : Std.HashSet α) (l : ρ) :
  Std.HashSet α

Inserts multiple mappings into the hash set by iterating over the given collection and calling insert. If the same key appears multiple times, the first occurrence takes precedence.

Note: this precedence behavior is true for HashSet and HashSet.Raw. The insertMany function on HashMap, DHashMap, HashMap.Raw and DHashMap.Raw behaves differently: it will prefer the last appearance.

🔗def
Std.HashSet.erase.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α}
  (m : Std.HashSet α) (a : α) : Std.HashSet α
Std.HashSet.erase.{u} {α : Type u}
  {x✝ : BEq α} {x✝¹ : Hashable α}
  (m : Std.HashSet α) (a : α) :
  Std.HashSet α

Removes the element if it exists.

🔗def
Std.HashSet.filter.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α}
  (f : α → Bool) (m : Std.HashSet α) : Std.HashSet α
Std.HashSet.filter.{u} {α : Type u}
  {x✝ : BEq α} {x✝¹ : Hashable α}
  (f : α → Bool) (m : Std.HashSet α) :
  Std.HashSet α

Removes all elements from the hash set for which the given function returns false.

🔗def
Std.HashSet.containsThenInsert.{u} {α : Type u} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m : Std.HashSet α) (a : α) : Bool × Std.HashSet α
Std.HashSet.containsThenInsert.{u}
  {α : Type u} {x✝ : BEq α}
  {x✝¹ : Hashable α} (m : Std.HashSet α)
  (a : α) : Bool × Std.HashSet α

Checks whether an element is present in a set and inserts the element if it was not found. If the hash set already contains an element that is equal (with regard to ==) to the given element, then the hash set is returned unchanged.

Equivalent to (but potentially faster than) calling contains followed by insert.

🔗def
Std.HashSet.partition.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α}
  (f : α → Bool) (m : Std.HashSet α) : Std.HashSet α × Std.HashSet α
Std.HashSet.partition.{u} {α : Type u}
  {x✝ : BEq α} {x✝¹ : Hashable α}
  (f : α → Bool) (m : Std.HashSet α) :
  Std.HashSet α × Std.HashSet α

Partition a hashset into two hashsets based on a predicate.

🔗def
Std.HashSet.union.{u} {α : Type u} [BEq α] [Hashable α]
  (m₁ m₂ : Std.HashSet α) : Std.HashSet α
Std.HashSet.union.{u} {α : Type u} [BEq α]
  [Hashable α] (m₁ m₂ : Std.HashSet α) :
  Std.HashSet α

Computes the union of the given hash sets.

This function always merges the smaller set into the larger set, so the expected runtime is O(min(m₁.size, m₂.size)).

20.19.6.5. 迭代🔗

🔗def
Std.HashSet.iter.{u} {α : Type u} [BEq α] [Hashable α]
  (m : Std.HashSet α) : Std.Iter α
Std.HashSet.iter.{u} {α : Type u} [BEq α]
  [Hashable α] (m : Std.HashSet α) :
  Std.Iter α

Returns a finite iterator over the elements of a hash set. The iterator yields the elements of the set in order and then terminates.

Termination properties:

  • Finite instance: always

  • Productive instance: always

🔗def
Std.HashSet.all.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α}
  (m : Std.HashSet α) (p : α → Bool) : Bool
Std.HashSet.all.{u} {α : Type u}
  {x✝ : BEq α} {x✝¹ : Hashable α}
  (m : Std.HashSet α) (p : α → Bool) :
  Bool

Check if all elements satisfy the predicate, short-circuiting if a predicate fails.

🔗def
Std.HashSet.any.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α}
  (m : Std.HashSet α) (p : α → Bool) : Bool
Std.HashSet.any.{u} {α : Type u}
  {x✝ : BEq α} {x✝¹ : Hashable α}
  (m : Std.HashSet α) (p : α → Bool) :
  Bool

Check if any element satisfies the predicate, short-circuiting if a predicate succeeds.

🔗def
Std.HashSet.fold.{u, v} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α}
  {β : Type v} (f : β → α → β) (init : β) (m : Std.HashSet α) : β
Std.HashSet.fold.{u, v} {α : Type u}
  {x✝ : BEq α} {x✝¹ : Hashable α}
  {β : Type v} (f : β → α → β) (init : β)
  (m : Std.HashSet α) : β

Folds the given function over the elements of the hash set in some order.

🔗def
Std.HashSet.foldM.{u, v, w} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α}
  {m : Type v → Type w} [Monad m] {β : Type v} (f : β → α → m β)
  (init : β) (b : Std.HashSet α) : m β
Std.HashSet.foldM.{u, v, w} {α : Type u}
  {x✝ : BEq α} {x✝¹ : Hashable α}
  {m : Type v → Type w} [Monad m]
  {β : Type v} (f : β → α → m β)
  (init : β) (b : Std.HashSet α) : m β

Monadically computes a value by folding the given function over the elements in the hash set in some order.

🔗def
Std.HashSet.forIn.{u, v, w} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α}
  {m : Type v → Type w} [Monad m] {β : Type v}
  (f : α → β → m (ForInStep β)) (init : β) (b : Std.HashSet α) : m β
Std.HashSet.forIn.{u, v, w} {α : Type u}
  {x✝ : BEq α} {x✝¹ : Hashable α}
  {m : Type v → Type w} [Monad m]
  {β : Type v}
  (f : α → β → m (ForInStep β)) (init : β)
  (b : Std.HashSet α) : m β

Support for the for loop construct in do blocks.

🔗def
Std.HashSet.forM.{u, v, w} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α}
  {m : Type v → Type w} [Monad m] (f : α → m PUnit)
  (b : Std.HashSet α) : m PUnit
Std.HashSet.forM.{u, v, w} {α : Type u}
  {x✝ : BEq α} {x✝¹ : Hashable α}
  {m : Type v → Type w} [Monad m]
  (f : α → m PUnit) (b : Std.HashSet α) :
  m PUnit

Carries out a monadic action on each element in the hash set in some order.

20.19.6.6. 转换🔗

🔗def
Std.HashSet.ofList.{u} {α : Type u} [BEq α] [Hashable α] (l : List α) :
  Std.HashSet α
Std.HashSet.ofList.{u} {α : Type u}
  [BEq α] [Hashable α] (l : List α) :
  Std.HashSet α

Creates a hash set from a list of elements. Note that unlike repeatedly calling insert, if the collection contains multiple elements that are equal (with regard to ==), then the last element in the collection will be present in the returned hash set.

🔗def
Std.HashSet.toList.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α}
  (m : Std.HashSet α) : List α
Std.HashSet.toList.{u} {α : Type u}
  {x✝ : BEq α} {x✝¹ : Hashable α}
  (m : Std.HashSet α) : List α

Transforms the hash set into a list of elements in some order.

🔗def
Std.HashSet.ofArray.{u} {α : Type u} [BEq α] [Hashable α]
  (l : Array α) : Std.HashSet α
Std.HashSet.ofArray.{u} {α : Type u}
  [BEq α] [Hashable α] (l : Array α) :
  Std.HashSet α

Creates a hash set from an array of elements. Note that unlike repeatedly calling insert, if the collection contains multiple elements that are equal (with regard to ==), then the last element in the collection will be present in the returned hash set.

🔗def
Std.HashSet.toArray.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α}
  (m : Std.HashSet α) : Array α
Std.HashSet.toArray.{u} {α : Type u}
  {x✝ : BEq α} {x✝¹ : Hashable α}
  (m : Std.HashSet α) : Array α

Transforms the hash set into an array of elements in some order.

20.19.6.7. 非捆绑变体🔗

未捆绑的地图将格式良好的证明与数据分开。 这在定义 嵌套归纳类型 时主要有用。 要使用这些变体，请导入模块 Std.HashSet.Raw 和 Std.HashSet.RawLemmas。

🔗structure
Std.HashSet.Raw.{u} (α : Type u) : Type u
Std.HashSet.Raw.{u} (α : Type u) : Type u

Hash sets without a bundled well-formedness invariant, suitable for use in nested inductive types. The well-formedness invariant is called Raw.WF. When in doubt, prefer HashSet over HashSet.Raw. Lemmas about the operations on Std.Data.HashSet.Raw are available in the module Std.Data.HashSet.RawLemmas.

This is a simple separate-chaining hash table. The data of the hash set consists of a cached size and an array of buckets, where each bucket is a linked list of keys. The number of buckets is always a power of two. The hash set 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 set is used linearly to avoid expensive copies.

The hash set uses == (provided by the BEq typeclass) to compare elements 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.

Constructor

Std.HashSet.Raw.mk.{u}

Fields

inner : Std.HashMap.Raw α Unit

Internal implementation detail of the hash set.

🔗structure
Std.HashSet.Raw.WF.{u} {α : Type u} [BEq α] [Hashable α]
  (m : Std.HashSet.Raw α) : Prop
Std.HashSet.Raw.WF.{u} {α : Type u}
  [BEq α] [Hashable α]
  (m : Std.HashSet.Raw α) : Prop

Well-formedness predicate for hash sets. Users of HashSet will not need to interact with this. Users of HashSet.Raw will need to provide proofs of WF to lemmas and should use lemmas like WF.empty and WF.insert (which are always named exactly like the operations they are about) to show that set operations preserve well-formedness.

Constructor

Std.HashSet.Raw.WF.mk.{u}

Fields

out : m.inner.WF

Internal implementation detail of the hash set

20.19.7. 扩展哈希集🔗

🔗structure
Std.ExtHashSet.{u} (α : Type u) [BEq α] [Hashable α] : Type u
Std.ExtHashSet.{u} (α : Type u) [BEq α]
  [Hashable α] : Type u

Hash sets.

This is a simple separate-chaining hash table. The data of the hash set consists of a cached size and an array of buckets, where each bucket is a linked list of keys. The number of buckets is always a power of two. The hash set 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 set is used linearly to avoid expensive copies.

The hash set uses == (provided by the BEq typeclass) to compare elements 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.

In contrast to regular hash sets, Std.ExtHashSet offers several extensionality lemmas and therefore has more lemmas about equality of hash maps. This however also makes it lose the ability to iterate freely over hash sets.

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

Constructor

Std.ExtHashSet.mk.{u}

Fields

inner : Std.ExtHashMap α Unit

Internal implementation detail of the hash set.

20.19.7.1. 创建🔗

🔗def
Std.ExtHashSet.emptyWithCapacity.{u} {α : Type u} [BEq α] [Hashable α]
  (capacity : Nat := 8) : Std.ExtHashSet α
Std.ExtHashSet.emptyWithCapacity.{u}
  {α : Type u} [BEq α] [Hashable α]
  (capacity : Nat := 8) : Std.ExtHashSet α

Creates a new empty hash set. The optional parameter capacity can be supplied to presize the set so that it can hold the given number of elements without reallocating. It is also possible to use the empty collection notations ∅ and {} to create an empty hash set with the default capacity.

20.19.7.2. 特性🔗

🔗def
Std.ExtHashSet.isEmpty.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α}
  [EquivBEq α] [LawfulHashable α] (m : Std.ExtHashSet α) : Bool
Std.ExtHashSet.isEmpty.{u} {α : Type u}
  {x✝ : BEq α} {x✝¹ : Hashable α}
  [EquivBEq α] [LawfulHashable α]
  (m : Std.ExtHashSet α) : Bool

Returns true if the hash set contains no elements.

Note that if your BEq instance is not reflexive or your Hashable instance is not lawful, then it is possible that this function returns false even though m.contains a = false for all a.

🔗def
Std.ExtHashSet.size.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α}
  [EquivBEq α] [LawfulHashable α] (m : Std.ExtHashSet α) : Nat
Std.ExtHashSet.size.{u} {α : Type u}
  {x✝ : BEq α} {x✝¹ : Hashable α}
  [EquivBEq α] [LawfulHashable α]
  (m : Std.ExtHashSet α) : Nat

The number of elements present in the set

20.19.7.3. 查询🔗

🔗def
Std.ExtHashSet.contains.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α}
  [EquivBEq α] [LawfulHashable α] (m : Std.ExtHashSet α) (a : α) : Bool
Std.ExtHashSet.contains.{u} {α : Type u}
  {x✝ : BEq α} {x✝¹ : Hashable α}
  [EquivBEq α] [LawfulHashable α]
  (m : Std.ExtHashSet α) (a : α) : Bool

Returns true if the given key is present in the set. There is also a Prop-valued version of this: a ∈ m is equivalent to m.contains a = true.

Observe that this is different behavior than for lists: for lists, ∈ uses = and contains use == for comparisons, while for hash sets, both use ==.

🔗def
Std.ExtHashSet.get.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α}
  [EquivBEq α] [LawfulHashable α] (m : Std.ExtHashSet α) (a : α)
  (h : a ∈ m) : α
Std.ExtHashSet.get.{u} {α : Type u}
  {x✝ : BEq α} {x✝¹ : Hashable α}
  [EquivBEq α] [LawfulHashable α]
  (m : Std.ExtHashSet α) (a : α)
  (h : a ∈ m) : α

Retrieves the key from the set that matches a. Ensures that such a key exists by requiring a proof of a ∈ m. The result is guaranteed to be pointer equal to the key in the set.

🔗def
Std.ExtHashSet.get!.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α}
  [EquivBEq α] [LawfulHashable α] [Inhabited α] (m : Std.ExtHashSet α)
  (a : α) : α
Std.ExtHashSet.get!.{u} {α : Type u}
  {x✝ : BEq α} {x✝¹ : Hashable α}
  [EquivBEq α] [LawfulHashable α]
  [Inhabited α] (m : Std.ExtHashSet α)
  (a : α) : α

Checks if given key is contained and returns the key if it is, otherwise panics. If no panic occurs the result is guaranteed to be pointer equal to the key in the set.

🔗def
Std.ExtHashSet.get?.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α}
  [EquivBEq α] [LawfulHashable α] (m : Std.ExtHashSet α) (a : α) :
  Option α
Std.ExtHashSet.get?.{u} {α : Type u}
  {x✝ : BEq α} {x✝¹ : Hashable α}
  [EquivBEq α] [LawfulHashable α]
  (m : Std.ExtHashSet α) (a : α) :
  Option α

Checks if given key is contained and returns the key if it is, otherwise none. The result in the some case is guaranteed to be pointer equal to the key in the set.

🔗def
Std.ExtHashSet.getD.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α}
  [EquivBEq α] [LawfulHashable α] (m : Std.ExtHashSet α)
  (a fallback : α) : α
Std.ExtHashSet.getD.{u} {α : Type u}
  {x✝ : BEq α} {x✝¹ : Hashable α}
  [EquivBEq α] [LawfulHashable α]
  (m : Std.ExtHashSet α)
  (a fallback : α) : α

Checks if given key is contained and returns the key if it is, otherwise fallback. If they key is contained the result is guaranteed to be pointer equal to the key in the set.

20.19.7.4. 修改🔗

🔗def
Std.ExtHashSet.insert.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α}
  [EquivBEq α] [LawfulHashable α] (m : Std.ExtHashSet α) (a : α) :
  Std.ExtHashSet α
Std.ExtHashSet.insert.{u} {α : Type u}
  {x✝ : BEq α} {x✝¹ : Hashable α}
  [EquivBEq α] [LawfulHashable α]
  (m : Std.ExtHashSet α) (a : α) :
  Std.ExtHashSet α

Inserts the given element into the set. If the hash set already contains an element that is equal (with regard to ==) to the given element, then the hash set is returned unchanged.

Note: this non-replacement behavior is true for ExtHashSet and ExtHashSet.Raw. The insert function on ExtHashMap, DExtHashMap, ExtHashMap.Raw and DExtHashMap.Raw behaves differently: it will overwrite an existing mapping.

🔗def
Std.ExtHashSet.insertMany.{u, v} {α : Type u} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {ρ : Type v}
  [ForIn Id ρ α] (m : Std.ExtHashSet α) (l : ρ) : Std.ExtHashSet α
Std.ExtHashSet.insertMany.{u, v}
  {α : Type u} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α]
  [LawfulHashable α] {ρ : Type v}
  [ForIn Id ρ α] (m : Std.ExtHashSet α)
  (l : ρ) : Std.ExtHashSet α

Inserts multiple mappings into the hash set by iterating over the given collection and calling insert. If the same key appears multiple times, the first occurrence takes precedence.

Note: this precedence behavior is true for ExtHashSet and ExtHashSet.Raw. The insertMany function on ExtHashMap, DExtHashMap, ExtHashMap.Raw and DExtHashMap.Raw behaves differently: it will prefer the last appearance.

🔗def
Std.ExtHashSet.erase.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α}
  [EquivBEq α] [LawfulHashable α] (m : Std.ExtHashSet α) (a : α) :
  Std.ExtHashSet α
Std.ExtHashSet.erase.{u} {α : Type u}
  {x✝ : BEq α} {x✝¹ : Hashable α}
  [EquivBEq α] [LawfulHashable α]
  (m : Std.ExtHashSet α) (a : α) :
  Std.ExtHashSet α

Removes the element if it exists.

🔗def
Std.ExtHashSet.filter.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α}
  [EquivBEq α] [LawfulHashable α] (f : α → Bool)
  (m : Std.ExtHashSet α) : Std.ExtHashSet α
Std.ExtHashSet.filter.{u} {α : Type u}
  {x✝ : BEq α} {x✝¹ : Hashable α}
  [EquivBEq α] [LawfulHashable α]
  (f : α → Bool) (m : Std.ExtHashSet α) :
  Std.ExtHashSet α

Removes all elements from the hash set for which the given function returns false.

🔗def
Std.ExtHashSet.containsThenInsert.{u} {α : Type u} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]
  (m : Std.ExtHashSet α) (a : α) : Bool × Std.ExtHashSet α
Std.ExtHashSet.containsThenInsert.{u}
  {α : Type u} {x✝ : BEq α}
  {x✝¹ : Hashable α} [EquivBEq α]
  [LawfulHashable α]
  (m : Std.ExtHashSet α) (a : α) :
  Bool × Std.ExtHashSet α

Checks whether an element is present in a set and inserts the element if it was not found. If the hash set already contains an element that is equal (with regard to ==) to the given element, then the hash set is returned unchanged.

Equivalent to (but potentially faster than) calling contains followed by insert.

20.19.7.5. 转换🔗

🔗def
Std.ExtHashSet.ofList.{u} {α : Type u} [BEq α] [Hashable α]
  (l : List α) : Std.ExtHashSet α
Std.ExtHashSet.ofList.{u} {α : Type u}
  [BEq α] [Hashable α] (l : List α) :
  Std.ExtHashSet α

Creates a hash set from a list of elements. Note that unlike repeatedly calling insert, if the collection contains multiple elements that are equal (with regard to ==), then the last element in the collection will be present in the returned hash set.

🔗def
Std.ExtHashSet.ofArray.{u} {α : Type u} [BEq α] [Hashable α]
  (l : Array α) : Std.ExtHashSet α
Std.ExtHashSet.ofArray.{u} {α : Type u}
  [BEq α] [Hashable α] (l : Array α) :
  Std.ExtHashSet α

Creates a hash set from an array of elements. Note that unlike repeatedly calling insert, if the collection contains multiple elements that are equal (with regard to ==), then the last element in the collection will be present in the returned hash set.

20.19.8. 基于树的地图🔗

本节中的声明应使用 import Std.TreeMap 导入。

🔗structure
Std.TreeMap.{u, v} (α : Type u) (β : Type v)
  (cmp : α → α → Ordering := by exact compare) : Type (max u v)
Std.TreeMap.{u, v} (α : Type u)
  (β : Type v)
  (cmp : α → α → Ordering := by
    exact compare) :
  Type (max u v)

Tree maps.

A tree map stores an assignment of keys to values. It depends on a comparator function that defines an ordering on the keys and provides efficient order-dependent queries, such as retrieval of the minimum or maximum.

To ensure that the operations behave as expected, the comparator function cmp should satisfy certain laws that ensure a consistent ordering:

  • If a is less than (or equal) to b, then b is greater than (or equal) to a and vice versa (see the OrientedCmp typeclass).

  • If a is less than or equal to b and b is, in turn, less than or equal to c, then a is less than or equal to c (see the TransCmp typeclass).

Keys for which cmp a b = Ordering.eq are considered the same, i.e., there can be only one entry with key either a or b in a tree map. Looking up either a or b always yields the same entry, if any is present.

To avoid expensive copies, users should make sure that the tree map is used linearly.

Internally, the tree maps are represented as size-bounded trees, a type of self-balancing binary search tree with efficient order statistic lookups.

For use in proofs, the type Std.ExtTreeMap of extensional tree maps should be preferred. This type comes with several extensionality lemmas and provides the same functions but requires a TransCmp instance to work with.

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

20.19.8.1. 创建🔗

🔗def
Std.TreeMap.empty.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} : Std.TreeMap α β cmp
Std.TreeMap.empty.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering} :
  Std.TreeMap α β cmp

Creates a new empty tree map. It is also possible and recommended to use the empty collection notations ∅ and {} to create an empty tree map. simp replaces empty with ∅.

20.19.8.2. 特性🔗

🔗def
Std.TreeMap.size.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) : Nat
Std.TreeMap.size.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp) : Nat

Returns the number of mappings present in the map.

🔗def
Std.TreeMap.isEmpty.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) : Bool
Std.TreeMap.isEmpty.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp) : Bool

Returns true if the tree map contains no mappings.

20.19.8.3. 查询🔗

🔗def
Std.TreeMap.contains.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (l : Std.TreeMap α β cmp) (a : α) : Bool
Std.TreeMap.contains.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  (l : Std.TreeMap α β cmp) (a : α) : Bool

Returns true if there is a mapping for the given key a or a key that is equal to a according to the comparator cmp. There is also a Prop-valued version of this: a ∈ t is equivalent to t.contains a = true.

Observe that this is different behavior than for lists: for lists, ∈ uses = and contains uses == for equality checks, while for tree maps, both use the given comparator cmp.

🔗def
Std.TreeMap.get.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) (a : α)
  (h : a ∈ t) : β
Std.TreeMap.get.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp) (a : α)
  (h : a ∈ t) : β

Given a proof that a mapping for the given key is present, retrieves the mapping for the given key.

Uses the LawfulEqCmp instance to cast the retrieved value to the correct type.

🔗def
Std.TreeMap.get!.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} [Inhabited β] (t : Std.TreeMap α β cmp)
  (a : α) : β
Std.TreeMap.get!.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  [Inhabited β] (t : Std.TreeMap α β cmp)
  (a : α) : β

Tries to retrieve the mapping for the given key, panicking if no such mapping is present.

Uses the LawfulEqCmp instance to cast the retrieved value to the correct type.

🔗def
Std.TreeMap.get?.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) (a : α) : Option β
Std.TreeMap.get?.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp) (a : α) :
  Option β

Tries to retrieve the mapping for the given key, returning none if no such mapping is present.

Uses the LawfulEqCmp instance to cast the retrieved value to the correct type.

🔗def
Std.TreeMap.getD.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) (a : α)
  (fallback : β) : β
Std.TreeMap.getD.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp) (a : α)
  (fallback : β) : β

Tries to retrieve the mapping for the given key, returning fallback if no such mapping is present.

Uses the LawfulEqCmp instance to cast the retrieved value to the correct type.

🔗def
Std.TreeMap.getKey.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) (a : α)
  (h : a ∈ t) : α
Std.TreeMap.getKey.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp) (a : α)
  (h : a ∈ t) : α

Retrieves the key from the mapping that matches a. Ensures that such a mapping exists by requiring a proof of a ∈ m. The result is guaranteed to be pointer equal to the key in the map.

🔗def
Std.TreeMap.getKey!.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} [Inhabited α] (t : Std.TreeMap α β cmp)
  (a : α) : α
Std.TreeMap.getKey!.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  [Inhabited α] (t : Std.TreeMap α β cmp)
  (a : α) : α

Checks if a mapping for the given key exists and returns the key if it does, otherwise panics. If no panic occurs the result is guaranteed to be pointer equal to the key in the map.

🔗def
Std.TreeMap.getKey?.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) (a : α) : Option α
Std.TreeMap.getKey?.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp) (a : α) :
  Option α

Checks if a mapping for the given key exists and returns the key if it does, otherwise none. The result in the some case is guaranteed to be pointer equal to the key in the map.

🔗def
Std.TreeMap.getKeyD.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) (a fallback : α) :
  α
Std.TreeMap.getKeyD.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp)
  (a fallback : α) : α

Checks if a mapping for the given key exists and returns the key if it does, otherwise fallback. If a mapping exists the result is guaranteed to be pointer equal to the key in the map.

🔗def
Std.TreeMap.keys.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) : List α
Std.TreeMap.keys.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp) : List α

Returns a list of all keys present in the tree map in ascending order.

🔗def
Std.TreeMap.keysArray.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) : Array α
Std.TreeMap.keysArray.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp) : Array α

Returns an array of all keys present in the tree map in ascending order.

🔗def
Std.TreeMap.values.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) : List β
Std.TreeMap.values.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp) : List β

Returns a list of all values present in the tree map in ascending order.

🔗def
Std.TreeMap.valuesArray.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) : Array β
Std.TreeMap.valuesArray.{u, v}
  {α : Type u} {β : Type v}
  {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp) : Array β

Returns an array of all values present in the tree map in ascending order.

20.19.8.3.1. 基于排序的查询🔗

🔗def
Std.TreeMap.entryAtIdx.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) (n : Nat)
  (h : n < t.size) : α × β
Std.TreeMap.entryAtIdx.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp) (n : Nat)
  (h : n < t.size) : α × β

Returns the key-value pair with the n-th smallest key.

🔗def
Std.TreeMap.entryAtIdx!.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} [Inhabited (α × β)] (t : Std.TreeMap α β cmp)
  (n : Nat) : α × β
Std.TreeMap.entryAtIdx!.{u, v}
  {α : Type u} {β : Type v}
  {cmp : α → α → Ordering}
  [Inhabited (α × β)]
  (t : Std.TreeMap α β cmp) (n : Nat) :
  α × β

Returns the key-value pair with the n-th smallest key, or panics if n is at least t.size.

🔗def
Std.TreeMap.entryAtIdx?.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) (n : Nat) :
  Option (α × β)
Std.TreeMap.entryAtIdx?.{u, v}
  {α : Type u} {β : Type v}
  {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp) (n : Nat) :
  Option (α × β)

Returns the key-value pair with the n-th smallest key, or none if n is at least t.size.

🔗def
Std.TreeMap.entryAtIdxD.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) (n : Nat)
  (fallback : α × β) : α × β
Std.TreeMap.entryAtIdxD.{u, v}
  {α : Type u} {β : Type v}
  {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp) (n : Nat)
  (fallback : α × β) : α × β

Returns the key-value pair with the n-th smallest key, or fallback if n is at least t.size.

🔗def
Std.TreeMap.getEntryGE.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} [Std.TransCmp cmp] (t : Std.TreeMap α β cmp)
  (k : α) (h : ∃ a, a ∈ t ∧ (cmp a k).isGE = true) : α × β
Std.TreeMap.getEntryGE.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  [Std.TransCmp cmp]
  (t : Std.TreeMap α β cmp) (k : α)
  (h :
    ∃ a, a ∈ t ∧ (cmp a k).isGE = true) :
  α × β

Given a proof that such a mapping exists, retrieves the key-value pair with the smallest key that is greater than or equal to the given key.

🔗def
Std.TreeMap.getEntryGE!.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} [Inhabited (α × β)] (t : Std.TreeMap α β cmp)
  (k : α) : α × β
Std.TreeMap.getEntryGE!.{u, v}
  {α : Type u} {β : Type v}
  {cmp : α → α → Ordering}
  [Inhabited (α × β)]
  (t : Std.TreeMap α β cmp) (k : α) :
  α × β

Tries to retrieve the key-value pair with the smallest key that is greater than or equal to the given key, panicking if no such pair exists.

🔗def
Std.TreeMap.getEntryGE?.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) (k : α) :
  Option (α × β)
Std.TreeMap.getEntryGE?.{u, v}
  {α : Type u} {β : Type v}
  {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp) (k : α) :
  Option (α × β)

Tries to retrieve the key-value pair with the smallest key that is greater than or equal to the given key, returning none if no such pair exists.

🔗def
Std.TreeMap.getEntryGED.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) (k : α)
  (fallback : α × β) : α × β
Std.TreeMap.getEntryGED.{u, v}
  {α : Type u} {β : Type v}
  {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp) (k : α)
  (fallback : α × β) : α × β

Tries to retrieve the key-value pair with the smallest key that is greater than or equal to the given key, returning fallback if no such pair exists.

🔗def
Std.TreeMap.getEntryGT.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} [Std.TransCmp cmp] (t : Std.TreeMap α β cmp)
  (k : α) (h : ∃ a, a ∈ t ∧ cmp a k = Ordering.gt) : α × β
Std.TreeMap.getEntryGT.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  [Std.TransCmp cmp]
  (t : Std.TreeMap α β cmp) (k : α)
  (h :
    ∃ a, a ∈ t ∧ cmp a k = Ordering.gt) :
  α × β

Given a proof that such a mapping exists, retrieves the key-value pair with the smallest key that is greater than the given key.

🔗def
Std.TreeMap.getEntryGT!.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} [Inhabited (α × β)] (t : Std.TreeMap α β cmp)
  (k : α) : α × β
Std.TreeMap.getEntryGT!.{u, v}
  {α : Type u} {β : Type v}
  {cmp : α → α → Ordering}
  [Inhabited (α × β)]
  (t : Std.TreeMap α β cmp) (k : α) :
  α × β

Tries to retrieve the key-value pair with the smallest key that is greater than the given key, panicking if no such pair exists.

🔗def
Std.TreeMap.getEntryGT?.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) (k : α) :
  Option (α × β)
Std.TreeMap.getEntryGT?.{u, v}
  {α : Type u} {β : Type v}
  {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp) (k : α) :
  Option (α × β)

Tries to retrieve the key-value pair with the smallest key that is greater than the given key, returning none if no such pair exists.

🔗def
Std.TreeMap.getEntryGTD.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) (k : α)
  (fallback : α × β) : α × β
Std.TreeMap.getEntryGTD.{u, v}
  {α : Type u} {β : Type v}
  {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp) (k : α)
  (fallback : α × β) : α × β

Tries to retrieve the key-value pair with the smallest key that is greater than the given key, returning fallback if no such pair exists.

🔗def
Std.TreeMap.getEntryLE.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} [Std.TransCmp cmp] (t : Std.TreeMap α β cmp)
  (k : α) (h : ∃ a, a ∈ t ∧ (cmp a k).isLE = true) : α × β
Std.TreeMap.getEntryLE.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  [Std.TransCmp cmp]
  (t : Std.TreeMap α β cmp) (k : α)
  (h :
    ∃ a, a ∈ t ∧ (cmp a k).isLE = true) :
  α × β

Given a proof that such a mapping exists, retrieves the key-value pair with the largest key that is less than or equal to the given key.

🔗def
Std.TreeMap.getEntryLE!.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} [Inhabited (α × β)] (t : Std.TreeMap α β cmp)
  (k : α) : α × β
Std.TreeMap.getEntryLE!.{u, v}
  {α : Type u} {β : Type v}
  {cmp : α → α → Ordering}
  [Inhabited (α × β)]
  (t : Std.TreeMap α β cmp) (k : α) :
  α × β

Tries to retrieve the key-value pair with the largest key that is less than or equal to the given key, panicking if no such pair exists.

🔗def
Std.TreeMap.getEntryLE?.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) (k : α) :
  Option (α × β)
Std.TreeMap.getEntryLE?.{u, v}
  {α : Type u} {β : Type v}
  {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp) (k : α) :
  Option (α × β)

Tries to retrieve the key-value pair with the largest key that is less than or equal to the given key, returning none if no such pair exists.

🔗def
Std.TreeMap.getEntryLED.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) (k : α)
  (fallback : α × β) : α × β
Std.TreeMap.getEntryLED.{u, v}
  {α : Type u} {β : Type v}
  {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp) (k : α)
  (fallback : α × β) : α × β

Tries to retrieve the key-value pair with the largest key that is less than or equal to the given key, returning fallback if no such pair exists.

🔗def
Std.TreeMap.getEntryLT.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} [Std.TransCmp cmp] (t : Std.TreeMap α β cmp)
  (k : α) (h : ∃ a, a ∈ t ∧ cmp a k = Ordering.lt) : α × β
Std.TreeMap.getEntryLT.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  [Std.TransCmp cmp]
  (t : Std.TreeMap α β cmp) (k : α)
  (h :
    ∃ a, a ∈ t ∧ cmp a k = Ordering.lt) :
  α × β

Given a proof that such a mapping exists, retrieves the key-value pair with the largest key that is less than the given key.

🔗def
Std.TreeMap.getEntryLT!.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} [Inhabited (α × β)] (t : Std.TreeMap α β cmp)
  (k : α) : α × β
Std.TreeMap.getEntryLT!.{u, v}
  {α : Type u} {β : Type v}
  {cmp : α → α → Ordering}
  [Inhabited (α × β)]
  (t : Std.TreeMap α β cmp) (k : α) :
  α × β

Tries to retrieve the key-value pair with the largest key that is less than the given key, panicking if no such pair exists.

🔗def
Std.TreeMap.getEntryLT?.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) (k : α) :
  Option (α × β)
Std.TreeMap.getEntryLT?.{u, v}
  {α : Type u} {β : Type v}
  {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp) (k : α) :
  Option (α × β)

Tries to retrieve the key-value pair with the largest key that is less than the given key, returning none if no such pair exists.

🔗def
Std.TreeMap.getEntryLTD.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) (k : α)
  (fallback : α × β) : α × β
Std.TreeMap.getEntryLTD.{u, v}
  {α : Type u} {β : Type v}
  {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp) (k : α)
  (fallback : α × β) : α × β

Tries to retrieve the key-value pair with the largest key that is less than the given key, returning fallback if no such pair exists.

🔗def
Std.TreeMap.getKeyGE.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} [Std.TransCmp cmp] (t : Std.TreeMap α β cmp)
  (k : α) (h : ∃ a, a ∈ t ∧ (cmp a k).isGE = true) : α
Std.TreeMap.getKeyGE.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  [Std.TransCmp cmp]
  (t : Std.TreeMap α β cmp) (k : α)
  (h :
    ∃ a, a ∈ t ∧ (cmp a k).isGE = true) :
  α

Given a proof that such a mapping exists, retrieves the smallest key that is greater than or equal to the given key.

🔗def
Std.TreeMap.getKeyGE!.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} [Inhabited α] (t : Std.TreeMap α β cmp)
  (k : α) : α
Std.TreeMap.getKeyGE!.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  [Inhabited α] (t : Std.TreeMap α β cmp)
  (k : α) : α

Tries to retrieve the smallest key that is greater than or equal to the given key, panicking if no such key exists.

🔗def
Std.TreeMap.getKeyGE?.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) (k : α) : Option α
Std.TreeMap.getKeyGE?.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp) (k : α) :
  Option α

Tries to retrieve the smallest key that is greater than or equal to the given key, returning none if no such key exists.

🔗def
Std.TreeMap.getKeyGED.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) (k fallback : α) :
  α
Std.TreeMap.getKeyGED.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp)
  (k fallback : α) : α

Tries to retrieve the smallest key that is greater than or equal to the given key, returning fallback if no such key exists.

🔗def
Std.TreeMap.getKeyGT.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} [Std.TransCmp cmp] (t : Std.TreeMap α β cmp)
  (k : α) (h : ∃ a, a ∈ t ∧ cmp a k = Ordering.gt) : α
Std.TreeMap.getKeyGT.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  [Std.TransCmp cmp]
  (t : Std.TreeMap α β cmp) (k : α)
  (h :
    ∃ a, a ∈ t ∧ cmp a k = Ordering.gt) :
  α

Given a proof that such a mapping exists, retrieves the smallest key that is greater than the given key.

🔗def
Std.TreeMap.getKeyGT!.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} [Inhabited α] (t : Std.TreeMap α β cmp)
  (k : α) : α
Std.TreeMap.getKeyGT!.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  [Inhabited α] (t : Std.TreeMap α β cmp)
  (k : α) : α

Tries to retrieve the smallest key that is greater than the given key, panicking if no such key exists.

🔗def
Std.TreeMap.getKeyGT?.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) (k : α) : Option α
Std.TreeMap.getKeyGT?.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp) (k : α) :
  Option α

Tries to retrieve the smallest key that is greater than the given key, returning none if no such key exists.

🔗def
Std.TreeMap.getKeyGTD.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) (k fallback : α) :
  α
Std.TreeMap.getKeyGTD.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp)
  (k fallback : α) : α

Tries to retrieve the smallest key that is greater than the given key, returning fallback if no such key exists.

🔗def
Std.TreeMap.getKeyLE.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} [Std.TransCmp cmp] (t : Std.TreeMap α β cmp)
  (k : α) (h : ∃ a, a ∈ t ∧ (cmp a k).isLE = true) : α
Std.TreeMap.getKeyLE.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  [Std.TransCmp cmp]
  (t : Std.TreeMap α β cmp) (k : α)
  (h :
    ∃ a, a ∈ t ∧ (cmp a k).isLE = true) :
  α

Given a proof that such a mapping exists, retrieves the largest key that is less than or equal to the given key.

🔗def
Std.TreeMap.getKeyLE!.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} [Inhabited α] (t : Std.TreeMap α β cmp)
  (k : α) : α
Std.TreeMap.getKeyLE!.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  [Inhabited α] (t : Std.TreeMap α β cmp)
  (k : α) : α

Tries to retrieve the largest key that is less than or equal to the given key, panicking if no such key exists.

🔗def
Std.TreeMap.getKeyLE?.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) (k : α) : Option α
Std.TreeMap.getKeyLE?.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp) (k : α) :
  Option α

Tries to retrieve the largest key that is less than or equal to the given key, returning none if no such key exists.

🔗def
Std.TreeMap.getKeyLED.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) (k fallback : α) :
  α
Std.TreeMap.getKeyLED.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp)
  (k fallback : α) : α

Tries to retrieve the largest key that is less than or equal to the given key, returning fallback if no such key exists.

🔗def
Std.TreeMap.getKeyLT.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} [Std.TransCmp cmp] (t : Std.TreeMap α β cmp)
  (k : α) (h : ∃ a, a ∈ t ∧ cmp a k = Ordering.lt) : α
Std.TreeMap.getKeyLT.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  [Std.TransCmp cmp]
  (t : Std.TreeMap α β cmp) (k : α)
  (h :
    ∃ a, a ∈ t ∧ cmp a k = Ordering.lt) :
  α

Given a proof that such a mapping exists, retrieves the largest key that is less than the given key.

🔗def
Std.TreeMap.getKeyLT!.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} [Inhabited α] (t : Std.TreeMap α β cmp)
  (k : α) : α
Std.TreeMap.getKeyLT!.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  [Inhabited α] (t : Std.TreeMap α β cmp)
  (k : α) : α

Tries to retrieve the largest key that is less than the given key, panicking if no such key exists.

🔗def
Std.TreeMap.getKeyLT?.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) (k : α) : Option α
Std.TreeMap.getKeyLT?.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp) (k : α) :
  Option α

Tries to retrieve the largest key that is less than the given key, returning none if no such key exists.

🔗def
Std.TreeMap.getKeyLTD.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) (k fallback : α) :
  α
Std.TreeMap.getKeyLTD.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp)
  (k fallback : α) : α

Tries to retrieve the largest key that is less than the given key, returning fallback if no such key exists.

🔗def
Std.TreeMap.keyAtIdx.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) (n : Nat)
  (h : n < t.size) : α
Std.TreeMap.keyAtIdx.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp) (n : Nat)
  (h : n < t.size) : α

Returns the n-th smallest key.

🔗def
Std.TreeMap.keyAtIdx!.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} [Inhabited α] (t : Std.TreeMap α β cmp)
  (n : Nat) : α
Std.TreeMap.keyAtIdx!.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  [Inhabited α] (t : Std.TreeMap α β cmp)
  (n : Nat) : α

Returns the n-th smallest key, or panics if n is at least t.size.

🔗def
Std.TreeMap.keyAtIdx?.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) (n : Nat) :
  Option α
Std.TreeMap.keyAtIdx?.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp) (n : Nat) :
  Option α

Returns the n-th smallest key, or none if n is at least t.size.

🔗def
Std.TreeMap.keyAtIdxD.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) (n : Nat)
  (fallback : α) : α
Std.TreeMap.keyAtIdxD.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp) (n : Nat)
  (fallback : α) : α

Returns the n-th smallest key, or fallback if n is at least t.size.

🔗def
Std.TreeMap.minEntry.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp)
  (h : t.isEmpty = false) : α × β
Std.TreeMap.minEntry.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp)
  (h : t.isEmpty = false) : α × β

Given a proof that the tree map is not empty, retrieves the key-value pair with the smallest key.

🔗def
Std.TreeMap.minEntry!.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} [Inhabited (α × β)]
  (t : Std.TreeMap α β cmp) : α × β
Std.TreeMap.minEntry!.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  [Inhabited (α × β)]
  (t : Std.TreeMap α β cmp) : α × β

Tries to retrieve the key-value pair with the smallest key in the tree map, panicking if the map is empty.

🔗def
Std.TreeMap.minEntry?.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) : Option (α × β)
Std.TreeMap.minEntry?.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp) :
  Option (α × β)

Tries to retrieve the key-value pair with the smallest key in the tree map, returning none if the map is empty.

🔗def
Std.TreeMap.minEntryD.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp)
  (fallback : α × β) : α × β
Std.TreeMap.minEntryD.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp)
  (fallback : α × β) : α × β

Tries to retrieve the key-value pair with the smallest key in the tree map, returning fallback if the tree map is empty.

🔗def
Std.TreeMap.minKey.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp)
  (h : t.isEmpty = false) : α
Std.TreeMap.minKey.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp)
  (h : t.isEmpty = false) : α

Given a proof that the tree map is not empty, retrieves the smallest key.

🔗def
Std.TreeMap.minKey!.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} [Inhabited α] (t : Std.TreeMap α β cmp) : α
Std.TreeMap.minKey!.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  [Inhabited α]
  (t : Std.TreeMap α β cmp) : α

Tries to retrieve the smallest key in the tree map, panicking if the map is empty.

🔗def
Std.TreeMap.minKey?.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) : Option α
Std.TreeMap.minKey?.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp) : Option α

Tries to retrieve the smallest key in the tree map, returning none if the map is empty.

🔗def
Std.TreeMap.minKeyD.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) (fallback : α) : α
Std.TreeMap.minKeyD.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp)
  (fallback : α) : α

Tries to retrieve the smallest key in the tree map, returning fallback if the tree map is empty.

🔗def
Std.TreeMap.maxEntry.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp)
  (h : t.isEmpty = false) : α × β
Std.TreeMap.maxEntry.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp)
  (h : t.isEmpty = false) : α × β

Given a proof that the tree map is not empty, retrieves the key-value pair with the largest key.

🔗def
Std.TreeMap.maxEntry!.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} [Inhabited (α × β)]
  (t : Std.TreeMap α β cmp) : α × β
Std.TreeMap.maxEntry!.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  [Inhabited (α × β)]
  (t : Std.TreeMap α β cmp) : α × β

Tries to retrieve the key-value pair with the largest key in the tree map, panicking if the map is empty.

🔗def
Std.TreeMap.maxEntry?.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) : Option (α × β)
Std.TreeMap.maxEntry?.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp) :
  Option (α × β)

Tries to retrieve the key-value pair with the largest key in the tree map, returning none if the map is empty.

🔗def
Std.TreeMap.maxEntryD.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp)
  (fallback : α × β) : α × β
Std.TreeMap.maxEntryD.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp)
  (fallback : α × β) : α × β

Tries to retrieve the key-value pair with the largest key in the tree map, returning fallback if the tree map is empty.

🔗def
Std.TreeMap.maxKey.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp)
  (h : t.isEmpty = false) : α
Std.TreeMap.maxKey.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp)
  (h : t.isEmpty = false) : α

Given a proof that the tree map is not empty, retrieves the largest key.

🔗def
Std.TreeMap.maxKey!.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} [Inhabited α] (t : Std.TreeMap α β cmp) : α
Std.TreeMap.maxKey!.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  [Inhabited α]
  (t : Std.TreeMap α β cmp) : α

Tries to retrieve the largest key in the tree map, panicking if the map is empty.

🔗def
Std.TreeMap.maxKey?.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) : Option α
Std.TreeMap.maxKey?.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp) : Option α

Tries to retrieve the largest key in the tree map, returning none if the map is empty.

🔗def
Std.TreeMap.maxKeyD.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) (fallback : α) : α
Std.TreeMap.maxKeyD.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp)
  (fallback : α) : α

Tries to retrieve the largest key in the tree map, returning fallback if the tree map is empty.

20.19.8.4. 修改🔗

🔗def
Std.TreeMap.alter.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) (a : α)
  (f : Option β → Option β) : Std.TreeMap α β cmp
Std.TreeMap.alter.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp) (a : α)
  (f : Option β → Option β) :
  Std.TreeMap α β cmp

Modifies in place the value associated with a given key, allowing creating new values and deleting values via an Option valued replacement function.

This function ensures that the value is used linearly.

🔗def
Std.TreeMap.modify.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) (a : α)
  (f : β → β) : Std.TreeMap α β cmp
Std.TreeMap.modify.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp) (a : α)
  (f : β → β) : Std.TreeMap α β cmp

Modifies in place the value associated with a given key.

This function ensures that the value is used linearly.

🔗def
Std.TreeMap.containsThenInsert.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) (a : α) (b : β) :
  Bool × Std.TreeMap α β cmp
Std.TreeMap.containsThenInsert.{u, v}
  {α : Type u} {β : Type v}
  {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp) (a : α)
  (b : β) : Bool × Std.TreeMap α β cmp

Checks whether a key is present in a map and unconditionally inserts a value for the key.

Equivalent to (but potentially faster than) calling contains followed by insert.

🔗def
Std.TreeMap.containsThenInsertIfNew.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) (a : α) (b : β) :
  Bool × Std.TreeMap α β cmp
Std.TreeMap.containsThenInsertIfNew.{u, v}
  {α : Type u} {β : Type v}
  {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp) (a : α)
  (b : β) : Bool × Std.TreeMap α β cmp

Checks whether a key is present in a map and inserts a value for the key if it was not found. If the returned Bool is true, then the returned map is unaltered. If the Bool is false, then the returned map has a new value inserted.

Equivalent to (but potentially faster than) calling contains followed by insertIfNew.

🔗def
Std.TreeMap.erase.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) (a : α) :
  Std.TreeMap α β cmp
Std.TreeMap.erase.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp) (a : α) :
  Std.TreeMap α β cmp

Removes the mapping for the given key if it exists.

🔗def
Std.TreeMap.eraseMany.{u, v, u_1} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} {ρ : Type u_1} [ForIn Id ρ α]
  (t : Std.TreeMap α β cmp) (l : ρ) : Std.TreeMap α β cmp
Std.TreeMap.eraseMany.{u, v, u_1}
  {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} {ρ : Type u_1}
  [ForIn Id ρ α] (t : Std.TreeMap α β cmp)
  (l : ρ) : Std.TreeMap α β cmp

Erases multiple mappings from the tree map by iterating over the given collection and calling erase.

🔗def
Std.TreeMap.filter.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (f : α → β → Bool)
  (m : Std.TreeMap α β cmp) : Std.TreeMap α β cmp
Std.TreeMap.filter.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  (f : α → β → Bool)
  (m : Std.TreeMap α β cmp) :
  Std.TreeMap α β cmp

Removes all mappings of the map for which the given function returns false.

🔗def
Std.TreeMap.filterMap.{u, v, w} {α : Type u} {β : Type v} {γ : Type w}
  {cmp : α → α → Ordering} (f : α → β → Option γ)
  (m : Std.TreeMap α β cmp) : Std.TreeMap α γ cmp
Std.TreeMap.filterMap.{u, v, w}
  {α : Type u} {β : Type v} {γ : Type w}
  {cmp : α → α → Ordering}
  (f : α → β → Option γ)
  (m : Std.TreeMap α β cmp) :
  Std.TreeMap α γ cmp

Updates the values of the map by applying the given function to all mappings, keeping only those mappings where the function returns some value.

🔗def
Std.TreeMap.insert.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (l : Std.TreeMap α β cmp) (a : α) (b : β) :
  Std.TreeMap α β cmp
Std.TreeMap.insert.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  (l : Std.TreeMap α β cmp) (a : α)
  (b : β) : Std.TreeMap α β cmp

Inserts the given mapping into the map. If there is already a mapping for the given key, then both key and value will be replaced.

🔗def
Std.TreeMap.insertIfNew.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) (a : α) (b : β) :
  Std.TreeMap α β cmp
Std.TreeMap.insertIfNew.{u, v}
  {α : Type u} {β : Type v}
  {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp) (a : α)
  (b : β) : Std.TreeMap α β cmp

If there is no mapping for the given key, inserts the given mapping into the map. Otherwise, returns the map unaltered.

🔗def
Std.TreeMap.getThenInsertIfNew?.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) (a : α) (b : β) :
  Option β × Std.TreeMap α β cmp
Std.TreeMap.getThenInsertIfNew?.{u, v}
  {α : Type u} {β : Type v}
  {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp) (a : α)
  (b : β) : Option β × Std.TreeMap α β cmp

Checks whether a key is present in a map, returning the associated value, and inserts a value for the key if it was not found.

If the returned value is some v, then the returned map is unaltered. If it is none, then the returned map has a new value inserted.

Equivalent to (but potentially faster than) calling get? followed by insertIfNew.

Uses the LawfulEqCmp instance to cast the retrieved value to the correct type.

🔗def
Std.TreeMap.insertMany.{u, v, u_1} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} {ρ : Type u_1} [ForIn Id ρ (α × β)]
  (t : Std.TreeMap α β cmp) (l : ρ) : Std.TreeMap α β cmp
Std.TreeMap.insertMany.{u, v, u_1}
  {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} {ρ : Type u_1}
  [ForIn Id ρ (α × β)]
  (t : Std.TreeMap α β cmp) (l : ρ) :
  Std.TreeMap α β cmp

Inserts multiple mappings into the tree map by iterating over the given collection and calling insert. If the same key appears multiple times, the last occurrence takes precedence.

Note: this precedence behavior is true for TreeMap, DTreeMap, TreeMap.Raw and DTreeMap.Raw. The insertMany function on TreeSet and TreeSet.Raw behaves differently: it will prefer the first appearance.

🔗def
Std.TreeMap.insertManyIfNewUnit.{u, u_1} {α : Type u}
  {cmp : α → α → Ordering} {ρ : Type u_1} [ForIn Id ρ α]
  (t : Std.TreeMap α Unit cmp) (l : ρ) : Std.TreeMap α Unit cmp
Std.TreeMap.insertManyIfNewUnit.{u, u_1}
  {α : Type u} {cmp : α → α → Ordering}
  {ρ : Type u_1} [ForIn Id ρ α]
  (t : Std.TreeMap α Unit cmp) (l : ρ) :
  Std.TreeMap α Unit cmp

Inserts multiple elements into the tree map by iterating over the given collection and calling insertIfNew. If the same key appears multiple times, the first occurrence takes precedence.

🔗def
Std.TreeMap.mergeWith.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (mergeFn : α → β → β → β)
  (t₁ t₂ : Std.TreeMap α β cmp) : Std.TreeMap α β cmp
Std.TreeMap.mergeWith.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  (mergeFn : α → β → β → β)
  (t₁ t₂ : Std.TreeMap α β cmp) :
  Std.TreeMap α β cmp

Returns a map that contains all mappings of t₁ and t₂. In case that both maps contain the same key k with respect to cmp, the provided function is used to determine the new value from the respective values in t₁ and t₂.

This function ensures that t₁ is used linearly. It also uses the individual values in t₁ linearly if the merge function uses the second argument (i.e. the first of type β a) linearly. Hence, as long as t₁ is unshared, the performance characteristics follow the following imperative description: Iterate over all mappings in t₂, inserting them into t₁ if t₁ does not contain a conflicting mapping yet. If t₁ does contain a conflicting mapping, use the given merge function to merge the mapping in t₂ into the mapping in t₁. Then return t₁.

Hence, the runtime of this method scales logarithmically in the size of t₁ and linearly in the size of t₂ as long as t₁ is unshared.

🔗def
Std.TreeMap.partition.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (f : α → β → Bool)
  (t : Std.TreeMap α β cmp) : Std.TreeMap α β cmp × Std.TreeMap α β cmp
Std.TreeMap.partition.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  (f : α → β → Bool)
  (t : Std.TreeMap α β cmp) :
  Std.TreeMap α β cmp ×
    Std.TreeMap α β cmp

Partitions a tree map into two tree maps based on a predicate.

20.19.8.5. 迭代🔗

🔗def
Std.TreeMap.iter.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (m : Std.TreeMap α β cmp) : Std.Iter (α × β)
Std.TreeMap.iter.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  (m : Std.TreeMap α β cmp) :
  Std.Iter (α × β)

Returns a finite iterator over the entries of a tree map. The iterator yields the elements of the map in order and then terminates.

Termination properties:

  • Finite instance: always

  • Productive instance: always

🔗def
Std.TreeMap.keysIter.{u} {α β : Type u} {cmp : α → α → Ordering}
  (m : Std.TreeMap α β cmp) : Std.Iter α
Std.TreeMap.keysIter.{u} {α β : Type u}
  {cmp : α → α → Ordering}
  (m : Std.TreeMap α β cmp) : Std.Iter α

Returns a finite iterator over the keys of a tree map. The iterator yields the keys in order and then terminates.

The key and value types must live in the same universe.

Termination properties:

  • Finite instance: always

  • Productive instance: always

🔗def
Std.TreeMap.valuesIter.{u} {α β : Type u} {cmp : α → α → Ordering}
  (m : Std.TreeMap α β cmp) : Std.Iter β
Std.TreeMap.valuesIter.{u} {α β : Type u}
  {cmp : α → α → Ordering}
  (m : Std.TreeMap α β cmp) : Std.Iter β

Returns a finite iterator over the values of a tree map. The iterator yields the values in order and then terminates.

The key and value types must live in the same universe.

Termination properties:

  • Finite instance: always

  • Productive instance: always

🔗def
Std.TreeMap.map.{u, v, w} {α : Type u} {β : Type v} {γ : Type w}
  {cmp : α → α → Ordering} (f : α → β → γ) (t : Std.TreeMap α β cmp) :
  Std.TreeMap α γ cmp
Std.TreeMap.map.{u, v, w} {α : Type u}
  {β : Type v} {γ : Type w}
  {cmp : α → α → Ordering} (f : α → β → γ)
  (t : Std.TreeMap α β cmp) :
  Std.TreeMap α γ cmp

Updates the values of the map by applying the given function to all mappings.

🔗def
Std.TreeMap.all.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp)
  (p : α → β → Bool) : Bool
Std.TreeMap.all.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp)
  (p : α → β → Bool) : Bool

Check if all elements satisfy the predicate, short-circuiting if a predicate fails.

🔗def
Std.TreeMap.any.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp)
  (p : α → β → Bool) : Bool
Std.TreeMap.any.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp)
  (p : α → β → Bool) : Bool

Check if any element satisfies the predicate, short-circuiting if a predicate fails.

🔗def
Std.TreeMap.foldl.{u, v, w} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} {δ : Type w} (f : δ → α → β → δ) (init : δ)
  (t : Std.TreeMap α β cmp) : δ
Std.TreeMap.foldl.{u, v, w} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  {δ : Type w} (f : δ → α → β → δ)
  (init : δ) (t : Std.TreeMap α β cmp) : δ

Folds the given function over the mappings in the map in ascending order.

🔗def
Std.TreeMap.foldlM.{u, v, w, w₂} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} {δ : Type w} {m : Type w → Type w₂} [Monad m]
  (f : δ → α → β → m δ) (init : δ) (t : Std.TreeMap α β cmp) : m δ
Std.TreeMap.foldlM.{u, v, w, w₂}
  {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} {δ : Type w}
  {m : Type w → Type w₂} [Monad m]
  (f : δ → α → β → m δ) (init : δ)
  (t : Std.TreeMap α β cmp) : m δ

Folds the given monadic function over the mappings in the map in ascending order.

🔗def
Std.TreeMap.foldr.{u, v, w} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} {δ : Type w} (f : α → β → δ → δ) (init : δ)
  (t : Std.TreeMap α β cmp) : δ
Std.TreeMap.foldr.{u, v, w} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  {δ : Type w} (f : α → β → δ → δ)
  (init : δ) (t : Std.TreeMap α β cmp) : δ

Folds the given function over the mappings in the map in descending order.

🔗def
Std.TreeMap.foldrM.{u, v, w, w₂} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} {δ : Type w} {m : Type w → Type w₂} [Monad m]
  (f : α → β → δ → m δ) (init : δ) (t : Std.TreeMap α β cmp) : m δ
Std.TreeMap.foldrM.{u, v, w, w₂}
  {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} {δ : Type w}
  {m : Type w → Type w₂} [Monad m]
  (f : α → β → δ → m δ) (init : δ)
  (t : Std.TreeMap α β cmp) : m δ

Folds the given monadic function over the mappings in the map in descending order.

🔗def
Std.TreeMap.forIn.{u, v, w, w₂} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} {δ : Type w} {m : Type w → Type w₂} [Monad m]
  (f : α → β → δ → m (ForInStep δ)) (init : δ)
  (t : Std.TreeMap α β cmp) : m δ
Std.TreeMap.forIn.{u, v, w, w₂}
  {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} {δ : Type w}
  {m : Type w → Type w₂} [Monad m]
  (f : α → β → δ → m (ForInStep δ))
  (init : δ) (t : Std.TreeMap α β cmp) :
  m δ

Support for the for loop construct in do blocks. Iteration happens in ascending order.

🔗def
Std.TreeMap.forM.{u, v, w, w₂} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} {m : Type w → Type w₂} [Monad m]
  (f : α → β → m PUnit) (t : Std.TreeMap α β cmp) : m PUnit
Std.TreeMap.forM.{u, v, w, w₂}
  {α : Type u} {β : Type v}
  {cmp : α → α → Ordering}
  {m : Type w → Type w₂} [Monad m]
  (f : α → β → m PUnit)
  (t : Std.TreeMap α β cmp) : m PUnit

Carries out a monadic action on each mapping in the tree map in ascending order.

20.19.8.6. 转换🔗

🔗def
Std.TreeMap.ofList.{u, v} {α : Type u} {β : Type v} (l : List (α × β))
  (cmp : α → α → Ordering := by exact compare) : Std.TreeMap α β cmp
Std.TreeMap.ofList.{u, v} {α : Type u}
  {β : Type v} (l : List (α × β))
  (cmp : α → α → Ordering := by
    exact compare) :
  Std.TreeMap α β cmp

Transforms a list of mappings into a tree map.

🔗def
Std.TreeMap.toList.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) : List (α × β)
Std.TreeMap.toList.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp) : List (α × β)

Transforms the tree map into a list of mappings in ascending order.

🔗def
Std.TreeMap.ofArray.{u, v} {α : Type u} {β : Type v} (a : Array (α × β))
  (cmp : α → α → Ordering := by exact compare) : Std.TreeMap α β cmp
Std.TreeMap.ofArray.{u, v} {α : Type u}
  {β : Type v} (a : Array (α × β))
  (cmp : α → α → Ordering := by
    exact compare) :
  Std.TreeMap α β cmp

Transforms a list of mappings into a tree map.

🔗def
Std.TreeMap.toArray.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) : Array (α × β)
Std.TreeMap.toArray.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  (t : Std.TreeMap α β cmp) :
  Array (α × β)

Transforms the tree map into a list of mappings in ascending order.

🔗def
Std.TreeMap.unitOfArray.{u} {α : Type u} (a : Array α)
  (cmp : α → α → Ordering := by exact compare) : Std.TreeMap α Unit cmp
Std.TreeMap.unitOfArray.{u} {α : Type u}
  (a : Array α)
  (cmp : α → α → Ordering := by
    exact compare) :
  Std.TreeMap α Unit cmp

Transforms an array of keys into a tree map.

🔗def
Std.TreeMap.unitOfList.{u} {α : Type u} (l : List α)
  (cmp : α → α → Ordering := by exact compare) : Std.TreeMap α Unit cmp
Std.TreeMap.unitOfList.{u} {α : Type u}
  (l : List α)
  (cmp : α → α → Ordering := by
    exact compare) :
  Std.TreeMap α Unit cmp

Transforms a list of keys into a tree map.

20.19.8.6.1. 非捆绑变体🔗

未捆绑的地图将格式良好的证明与数据分开。 这在定义 嵌套归纳类型 时主要有用。 要使用这些变体，请导入模块 Std.TreeMap.Raw。

🔗structure
Std.TreeMap.Raw.{u, v} (α : Type u) (β : Type v)
  (cmp : α → α → Ordering := by exact compare) : Type (max u v)
Std.TreeMap.Raw.{u, v} (α : Type u)
  (β : Type v)
  (cmp : α → α → Ordering := by
    exact compare) :
  Type (max u v)

Tree maps without a bundled well-formedness invariant, suitable for use in nested inductive types. The well-formedness invariant is called Raw.WF. When in doubt, prefer TreeMap over TreeMap.Raw. Lemmas about the operations on Std.TreeMap.Raw are available in the module Std.Data.TreeMap.Raw.Lemmas.

A tree map stores an assignment of keys to values. It depends on a comparator function that defines an ordering on the keys and provides efficient order-dependent queries, such as retrieval of the minimum or maximum.

To ensure that the operations behave as expected, the comparator function cmp should satisfy certain laws that ensure a consistent ordering:

  • If a is less than (or equal) to b, then b is greater than (or equal) to a and vice versa (see the OrientedCmp typeclass).

  • If a is less than or equal to b and b is, in turn, less than or equal to c, then a is less than or equal to c (see the TransCmp typeclass).

Keys for which cmp a b = Ordering.eq are considered the same, i.e., there can be only one entry with key either a or b in a tree map. Looking up either a or b always yields the same entry, if any is present.

To avoid expensive copies, users should make sure that the tree map is used linearly.

Internally, the tree maps are represented as size-bounded trees, a type of self-balancing binary search tree with efficient order statistic lookups.

Constructor

Std.TreeMap.Raw.mk.{u, v}

Fields

inner : Std.DTreeMap.Raw α (fun x => β) cmp

Internal implementation detail of the tree map.

🔗structure
Std.TreeMap.Raw.WF.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} (t : Std.TreeMap.Raw α β cmp) : Prop
Std.TreeMap.Raw.WF.{u, v} {α : Type u}
  {β : Type v} {cmp : α → α → Ordering}
  (t : Std.TreeMap.Raw α β cmp) : Prop

Well-formedness predicate for tree maps. Users of TreeMap will not need to interact with this. Users of TreeMap.Raw will need to provide proofs of WF to lemmas and should use lemmas like WF.empty and WF.insert (which are always named exactly like the operations they are about) to show that map operations preserve well-formedness. The constructors of this type are internal implementation details and should not be accessed by users.

Constructor

Std.TreeMap.Raw.WF.mk.{u, v}

Fields

out : t.inner.WF

Internal implementation detail of the tree map.

20.19.9. 基于树的依赖图🔗

本节中的声明应使用 import Std.DTreeMap 导入。

🔗structure
Std.DTreeMap.{u, v} (α : Type u) (β : α → Type v)
  (cmp : α → α → Ordering := by exact compare) : Type (max u v)
Std.DTreeMap.{u, v} (α : Type u)
  (β : α → Type v)
  (cmp : α → α → Ordering := by
    exact compare) :
  Type (max u v)

Dependent tree maps.

A tree map stores an assignment of keys to values. It depends on a comparator function that defines an ordering on the keys and provides efficient order-dependent queries, such as retrieval of the minimum or maximum.

To ensure that the operations behave as expected, the comparator function cmp should satisfy certain laws that ensure a consistent ordering:

  • If a is less than (or equal) to b, then b is greater than (or equal) to a and vice versa (see the OrientedCmp typeclass).

  • If a is less than or equal to b and b is, in turn, less than or equal to c, then a is less than or equal to c (see the TransCmp typeclass).

Keys for which cmp a b = Ordering.eq are considered the same, i.e., there can be only one entry with key either a or b in a tree map. Looking up either a or b always yields the same entry, if any is present. The get operations of the dependent tree map additionally require a LawfulEqCmp instance to ensure that cmp a b = .eq always implies a = b, so that their respective value types are equal.

To avoid expensive copies, users should make sure that the tree map is used linearly.

Internally, the tree maps are represented as size-bounded trees, a type of self-balancing binary search tree with efficient order statistic lookups.

For use in proofs, the type Std.ExtDTreeMap of extensional dependent tree maps should be preferred. This type comes with several extensionality lemmas and provides the same functions but requires a TransCmp instance to work with.

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

20.19.9.1. 创建🔗

🔗def
Std.DTreeMap.empty.{u, v} {α : Type u} {β : α → Type v}
  {cmp : α → α → Ordering} : Std.DTreeMap α β cmp
Std.DTreeMap.empty.{u, v} {α : Type u}
  {β : α → Type v}
  {cmp : α → α → Ordering} :
  Std.DTreeMap α β cmp

Creates a new empty tree map. It is also possible and recommended to use the empty collection notations ∅ and {} to create an empty tree map. simp replaces empty with ∅.

20.19.9.2. 特性🔗

🔗def
Std.DTreeMap.size.{u, v} {α : Type u} {β : α → Type v}
  {cmp : α → α → Ordering} (t : Std.DTreeMap α β cmp) : Nat
Std.DTreeMap.size.{u, v} {α : Type u}
  {β : α → Type v}
  {cmp : α → α → Ordering}
  (t : Std.DTreeMap α β cmp) : Nat

Returns the number of mappings present in the map.

🔗def
Std.DTreeMap.isEmpty.{u, v} {α : Type u} {β : α → Type v}
  {cmp : α → α → Ordering} (t : Std.DTreeMap α β cmp) : Bool
Std.DTreeMap.isEmpty.{u, v} {α : Type u}
  {β : α → Type v}
  {cmp : α → α → Ordering}
  (t : Std.DTreeMap α β cmp) : Bool

Returns true if the tree map contains no mappings.

20.19.9.3. 查询🔗

🔗def
Std.DTreeMap.contains.{u, v} {α : Type u} {β : α → Type v}
  {cmp : α → α → Ordering} (t : Std.DTreeMap α β cmp) (a : α) : Bool
Std.DTreeMap.contains.{u, v} {α : Type u}
  {β : α → Type v}
  {cmp : α → α → Ordering}
  (t : Std.DTreeMap α β cmp) (a : α) :
  Bool

Returns true if there is a mapping for the given key a or a key that is equal to a according to the comparator cmp. There is also a Prop-valued version of this: a ∈ t is equivalent to t.contains a = true.

Observe that this is different behavior than for lists: for lists, ∈ uses = and contains uses == for equality checks, while for tree maps, both use the given comparator cmp.

🔗def
Std.DTreeMap.get.{u, v} {α : Type u} {β : α → Type v}
  {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp]
  (t : Std.DTreeMap α β cmp) (a : α) (h : a ∈ t) : β a
Std.DTreeMap.get.{u, v} {α : Type u}
  {β : α → Type v}
  {cmp : α → α → Ordering}
  [Std.LawfulEqCmp cmp]
  (t : Std.DTreeMap α β cmp) (a : α)
  (h : a ∈ t) : β a

Given a proof that a mapping for the given key is present, retrieves the mapping for the given key.

Uses the LawfulEqCmp instance to cast the retrieved value to the correct type.

🔗def
Std.DTreeMap.get!.{u, v} {α : Type u} {β : α → Type v}
  {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp]
  (t : Std.DTreeMap α β cmp) (a : α) [Inhabited (β a)] : β a
Std.DTreeMap.get!.{u, v} {α : Type u}
  {β : α → Type v}
  {cmp : α → α → Ordering}
  [Std.LawfulEqCmp cmp]
  (t : Std.DTreeMap α β cmp) (a : α)
  [Inhabited (β a)] : β a

Tries to retrieve the mapping for the given key, panicking if no such mapping is present.

Uses the LawfulEqCmp instance to cast the retrieved value to the correct type.

🔗def
Std.DTreeMap.get?.{u, v} {α : Type u} {β : α → Type v}
  {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp]
  (t : Std.DTreeMap α β cmp) (a : α) : Option (β a)
Std.DTreeMap.get?.{u, v} {α : Type u}
  {β : α → Type v}
  {cmp : α → α → Ordering}
  [Std.LawfulEqCmp cmp]
  (t : Std.DTreeMap α β cmp) (a : α) :
  Option (β a)

Tries to retrieve the mapping for the given key, returning none if no such mapping is present.

Uses the LawfulEqCmp instance to cast the retrieved value to the correct type.

🔗def
Std.DTreeMap.getD.{u, v} {α : Type u} {β : α → Type v}
  {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp]
  (t : Std.DTreeMap α β cmp) (a : α) (fallback : β a) : β a
Std.DTreeMap.getD.{u, v} {α : Type u}
  {β : α → Type v}
  {cmp : α → α → Ordering}
  [Std.LawfulEqCmp cmp]
  (t : Std.DTreeMap α β cmp) (a : α)
  (fallback : β a) : β a

Tries to retrieve the mapping for the given key, returning fallback if no such mapping is present.

Uses the LawfulEqCmp instance to cast the retrieved value to the correct type.

🔗def
Std.DTreeMap.getKey.{u, v} {α : Type u} {β : α → Type v}
  {cmp : α → α → Ordering} (t : Std.DTreeMap α β cmp) (a : α)
  (h : a ∈ t) : α
Std.DTreeMap.getKey.{u, v} {α : Type u}
  {β : α → Type v}
  {cmp : α → α → Ordering}
  (t : Std.DTreeMap α β cmp) (a : α)
  (h : a ∈ t) : α

Retrieves the key from the mapping that matches a. Ensures that such a mapping exists by requiring a proof of a ∈ m. The result is guaranteed to be pointer equal to the key in the map.

🔗def
Std.DTreeMap.getKey!.{u, v} {α : Type u} {β : α → Type v}
  {cmp : α → α → Ordering} [Inhabited α] (t : Std.DTreeMap α β cmp)
  (a : α) : α
Std.DTreeMap.getKey!.{u, v} {α : Type u}
  {β : α → Type v}
  {cmp : α → α → Ordering} [Inhabited α]
  (t : Std.DTreeMap α β cmp) (a : α) : α

Checks if a mapping for the given key exists and returns the key if it does, otherwise panics. If no panic occurs the result is guaranteed to be pointer equal to the key in the map.

🔗def
Std.DTreeMap.getKey?.{u, v} {α : Type u} {β : α → Type v}
  {cmp : α → α → Ordering} (t : Std.DTreeMap α β cmp) (a : α) : Option α
Std.DTreeMap.getKey?.{u, v} {α : Type u}
  {β : α → Type v}
  {cmp : α → α → Ordering}
  (t : Std.DTreeMap α β cmp) (a : α) :
  Option α

Checks if a mapping for the given key exists and returns the key if it does, otherwise none. The result in the some case is guaranteed to be pointer equal to the key in the map.

🔗def
Std.DTreeMap.getKeyD.{u, v} {α : Type u} {β : α → Type v}
  {cmp : α → α → Ordering} (t : Std.DTreeMap α β cmp) (a fallback : α) :
  α
Std.DTreeMap.getKeyD.{u, v} {α : Type u}
  {β : α → Type v}
  {cmp : α → α → Ordering}
  (t : Std.DTreeMap α β cmp)
  (a fallback : α) : α

Checks if a mapping for the given key exists and returns the key if it does, otherwise fallback. If a mapping exists the result is guaranteed to be pointer equal to the key in the map.

🔗def
Std.DTreeMap.keys.{u, v} {α : Type u} {β : α → Type v}
  {cmp : α → α → Ordering} (t : Std.DTreeMap α β cmp) : List α
Std.DTreeMap.keys.{u, v} {α : Type u}
  {β : α → Type v}
  {cmp : α → α → Ordering}
  (t : Std.DTreeMap α β cmp) : List α

Returns a list of all keys present in the tree map in ascending order.

🔗def
Std.DTreeMap.keysArray.{u, v} {α : Type u} {β : α → Type v}
  {cmp : α → α → Ordering} (t : Std.DTreeMap α β cmp) : Array α
Std.DTreeMap.keysArray.{u, v} {α : Type u}
  {β : α → Type v}
  {cmp : α → α → Ordering}
  (t : Std.DTreeMap α β cmp) : Array α

Returns an array of all keys present in the tree map in ascending order.

🔗def
Std.DTreeMap.values.{u, v} {α : Type u} {cmp : α → α → Ordering}
  {β : Type v} (t : Std.DTreeMap α (fun x => β) cmp) : List β
Std.DTreeMap.values.{u, v} {α : Type u}
  {cmp : α → α → Ordering} {β : Type v}
  (t : Std.DTreeMap α (fun x => β) cmp) :
  List β

Returns a list of all values present in the tree map in ascending order.

🔗def
Std.DTreeMap.valuesArray.{u, v} {α : Type u} {cmp : α → α → Ordering}
  {β : Type v} (t : Std.DTreeMap α (fun x => β) cmp) : Array β
Std.DTreeMap.valuesArray.{u, v}
  {α : Type u} {cmp : α → α → Ordering}
  {β : Type v}
  (t : Std.DTreeMap α (fun x => β) cmp) :
  Array β

Returns an array of all values present in the tree map in ascending order.

20.19.9.4. 修改🔗

🔗def
Std.DTreeMap.alter.{u, v} {α : Type u} {β : α → Type v}
  {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp]
  (t : Std.DTreeMap α β cmp) (a : α) (f : Option (β a) → Option (β a)) :
  Std.DTreeMap α β cmp
Std.DTreeMap.alter.{u, v} {α : Type u}
  {β : α → Type v}
  {cmp : α → α → Ordering}
  [Std.LawfulEqCmp cmp]
  (t : Std.DTreeMap α β cmp) (a : α)
  (f : Option (β a) → Option (β a)) :
  Std.DTreeMap α β cmp

Modifies in place the value associated with a given key, allowing creating new values and deleting values via an Option valued replacement function.

This function ensures that the value is used linearly.

🔗def
Std.DTreeMap.modify.{u, v} {α : Type u} {β : α → Type v}
  {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp]
  (t : Std.DTreeMap α β cmp) (a : α) (f : β a → β a) :
  Std.DTreeMap α β cmp
Std.DTreeMap.modify.{u, v} {α : Type u}
  {β : α → Type v}
  {cmp : α → α → Ordering}
  [Std.LawfulEqCmp cmp]
  (t : Std.DTreeMap α β cmp) (a : α)
  (f : β a → β a) : Std.DTreeMap α β cmp

Modifies in place the value associated with a given key.

This function ensures that the value is used linearly.

🔗def
Std.DTreeMap.containsThenInsert.{u, v} {α : Type u} {β : α → Type v}
  {cmp : α → α → Ordering} (t : Std.DTreeMap α β cmp) (a : α)
  (b : β a) : Bool × Std.DTreeMap α β cmp
Std.DTreeMap.containsThenInsert.{u, v}
  {α : Type u} {β : α → Type v}
  {cmp : α → α → Ordering}
  (t : Std.DTreeMap α β cmp) (a : α)
  (b : β a) : Bool × Std.DTreeMap α β cmp

Checks whether a key is present in a map and unconditionally inserts a value for the key.

Equivalent to (but potentially faster than) calling contains followed by insert.

🔗def
Std.DTreeMap.containsThenInsertIfNew.{u, v} {α : Type u}
  {β : α → Type v} {cmp : α → α → Ordering} (t : Std.DTreeMap α β cmp)
  (a : α) (b : β a) : Bool × Std.DTreeMap α β cmp
Std.DTreeMap.containsThenInsertIfNew.{u,
    v}
  {α : Type u} {β : α → Type v}
  {cmp : α → α → Ordering}
  (t : Std.DTreeMap α β cmp) (a : α)
  (b : β a) : Bool × Std.DTreeMap α β cmp

Checks whether a key is present in a map and inserts a value for the key if it was not found. If the returned Bool is true, then the returned map is unaltered. If the Bool is false, then the returned map has a new value inserted.

Equivalent to (but potentially faster than) calling contains followed by insertIfNew.

🔗def
Std.DTreeMap.erase.{u, v} {α : Type u} {β : α → Type v}
  {cmp : α → α → Ordering} (t : Std.DTreeMap α β cmp) (a : α) :
  Std.DTreeMap α β cmp
Std.DTreeMap.erase.{u, v} {α : Type u}
  {β : α → Type v}
  {cmp : α → α → Ordering}
  (t : Std.DTreeMap α β cmp) (a : α) :
  Std.DTreeMap α β cmp

Removes the mapping for the given key if it exists.

🔗def
Std.DTreeMap.filter.{u, v} {α : Type u} {β : α → Type v}
  {cmp : α → α → Ordering} (f : (a : α) → β a → Bool)
  (t : Std.DTreeMap α β cmp) : Std.DTreeMap α β cmp
Std.DTreeMap.filter.{u, v} {α : Type u}
  {β : α → Type v}
  {cmp : α → α → Ordering}
  (f : (a : α) → β a → Bool)
  (t : Std.DTreeMap α β cmp) :
  Std.DTreeMap α β cmp

Removes all mappings of the map for which the given function returns false.

🔗def
Std.DTreeMap.filterMap.{u, v, w} {α : Type u} {β : α → Type v}
  {γ : α → Type w} {cmp : α → α → Ordering}
  (f : (a : α) → β a → Option (γ a)) (t : Std.DTreeMap α β cmp) :
  Std.DTreeMap α γ cmp
Std.DTreeMap.filterMap.{u, v, w}
  {α : Type u} {β : α → Type v}
  {γ : α → Type w}
  {cmp : α → α → Ordering}
  (f : (a : α) → β a → Option (γ a))
  (t : Std.DTreeMap α β cmp) :
  Std.DTreeMap α γ cmp

Updates the values of the map by applying the given function to all mappings, keeping only those mappings where the function returns some value.

🔗def
Std.DTreeMap.insert.{u, v} {α : Type u} {β : α → Type v}
  {cmp : α → α → Ordering} (t : Std.DTreeMap α β cmp) (a : α)
  (b : β a) : Std.DTreeMap α β cmp
Std.DTreeMap.insert.{u, v} {α : Type u}
  {β : α → Type v}
  {cmp : α → α → Ordering}
  (t : Std.DTreeMap α β cmp) (a : α)
  (b : β a) : Std.DTreeMap α β cmp

Inserts the given mapping into the map. If there is already a mapping for the given key, then both key and value will be replaced.

🔗def
Std.DTreeMap.insertIfNew.{u, v} {α : Type u} {β : α → Type v}
  {cmp : α → α → Ordering} (t : Std.DTreeMap α β cmp) (a : α)
  (b : β a) : Std.DTreeMap α β cmp
Std.DTreeMap.insertIfNew.{u, v}
  {α : Type u} {β : α → Type v}
  {cmp : α → α → Ordering}
  (t : Std.DTreeMap α β cmp) (a : α)
  (b : β a) : Std.DTreeMap α β cmp

If there is no mapping for the given key, inserts the given mapping into the map. Otherwise, returns the map unaltered.

🔗def
Std.DTreeMap.getThenInsertIfNew?.{u, v} {α : Type u} {β : α → Type v}
  {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp]
  (t : Std.DTreeMap α β cmp) (a : α) (b : β a) :
  Option (β a) × Std.DTreeMap α β cmp
Std.DTreeMap.getThenInsertIfNew?.{u, v}
  {α : Type u} {β : α → Type v}
  {cmp : α → α → Ordering}
  [Std.LawfulEqCmp cmp]
  (t : Std.DTreeMap α β cmp) (a : α)
  (b : β a) :
  Option (β a) × Std.DTreeMap α β cmp

Checks whether a key is present in a map, returning the associated value, and inserts a value for the key if it was not found.

If the returned value is some v, then the returned map is unaltered. If it is none, then the returned map has a new value inserted.

Equivalent to (but potentially faster than) calling get? followed by insertIfNew.

Uses the LawfulEqCmp instance to cast the retrieved value to the correct type.

🔗def
Std.DTreeMap.insertMany.{u, v, u_1} {α : Type u} {β : α → Type v}
  {cmp : α → α → Ordering} {ρ : Type u_1} [ForIn Id ρ ((a : α) × β a)]
  (t : Std.DTreeMap α β cmp) (l : ρ) : Std.DTreeMap α β cmp
Std.DTreeMap.insertMany.{u, v, u_1}
  {α : Type u} {β : α → Type v}
  {cmp : α → α → Ordering} {ρ : Type u_1}
  [ForIn Id ρ ((a : α) × β a)]
  (t : Std.DTreeMap α β cmp) (l : ρ) :
  Std.DTreeMap α β cmp

Inserts multiple mappings into the tree map by iterating over the given collection and calling insert. If the same key appears multiple times, the last occurrence takes precedence.

Note: this precedence behavior is true for TreeMap, DTreeMap, TreeMap.Raw and DTreeMap.Raw. The insertMany function on TreeSet and TreeSet.Raw behaves differently: it will prefer the first appearance.

🔗def
Std.DTreeMap.partition.{u, v} {α : Type u} {β : α → Type v}
  {cmp : α → α → Ordering} (f : (a : α) → β a → Bool)
  (t : Std.DTreeMap α β cmp) :
  Std.DTreeMap α β cmp × Std.DTreeMap α β cmp
Std.DTreeMap.partition.{u, v} {α : Type u}
  {β : α → Type v}
  {cmp : α → α → Ordering}
  (f : (a : α) → β a → Bool)
  (t : Std.DTreeMap α β cmp) :
  Std.DTreeMap α β cmp ×
    Std.DTreeMap α β cmp

Partitions a tree map into two tree maps based on a predicate.

20.19.9.5. 迭代🔗

🔗def
Std.DTreeMap.iter.{u, v} {α : Type u} {β : α → Type v}
  {cmp : α → α → Ordering} (m : Std.DTreeMap α β cmp) :
  Std.Iter ((a : α) × β a)
Std.DTreeMap.iter.{u, v} {α : Type u}
  {β : α → Type v}
  {cmp : α → α → Ordering}
  (m : Std.DTreeMap α β cmp) :
  Std.Iter ((a : α) × β a)

Returns a finite iterator over the entries of a dependent tree map. The iterator yields the elements of the map in order and then terminates.

Termination properties:

  • Finite instance: always

  • Productive instance: always

🔗def
Std.DTreeMap.keysIter.{u} {α : Type u} {β : α → Type u}
  {cmp : α → α → Ordering} (m : Std.DTreeMap α β cmp) : Std.Iter α
Std.DTreeMap.keysIter.{u} {α : Type u}
  {β : α → Type u}
  {cmp : α → α → Ordering}
  (m : Std.DTreeMap α β cmp) : Std.Iter α

Returns a finite iterator over the keys of a dependent tree map. The iterator yields the keys in order and then terminates.

The key and value types must live in the same universe.

Termination properties:

  • Finite instance: always

  • Productive instance: always

🔗def
Std.DTreeMap.valuesIter.{u} {α β : Type u} {cmp : α → α → Ordering}
  (m : Std.DTreeMap α (fun x => β) cmp) : Std.Iter β
Std.DTreeMap.valuesIter.{u} {α β : Type u}
  {cmp : α → α → Ordering}
  (m : Std.DTreeMap α (fun x => β) cmp) :
  Std.Iter β

Returns a finite iterator over the values of a tree map. The iterator yields the values in order and then terminates.

The key and value types must live in the same universe.

Termination properties:

  • Finite instance: always

  • Productive instance: always

🔗def
Std.DTreeMap.map.{u, v, w} {α : Type u} {β : α → Type v}
  {γ : α → Type w} {cmp : α → α → Ordering} (f : (a : α) → β a → γ a)
  (t : Std.DTreeMap α β cmp) : Std.DTreeMap α γ cmp
Std.DTreeMap.map.{u, v, w} {α : Type u}
  {β : α → Type v} {γ : α → Type w}
  {cmp : α → α → Ordering}
  (f : (a : α) → β a → γ a)
  (t : Std.DTreeMap α β cmp) :
  Std.DTreeMap α γ cmp

Updates the values of the map by applying the given function to all mappings.

🔗def
Std.DTreeMap.foldl.{u, v, w} {α : Type u} {β : α → Type v}
  {cmp : α → α → Ordering} {δ : Type w} (f : δ → (a : α) → β a → δ)
  (init : δ) (t : Std.DTreeMap α β cmp) : δ
Std.DTreeMap.foldl.{u, v, w} {α : Type u}
  {β : α → Type v}
  {cmp : α → α → Ordering} {δ : Type w}
  (f : δ → (a : α) → β a → δ) (init : δ)
  (t : Std.DTreeMap α β cmp) : δ

Folds the given function over the mappings in the map in ascending order.

🔗def
Std.DTreeMap.foldlM.{u, v, w, w₂} {α : Type u} {β : α → Type v}
  {cmp : α → α → Ordering} {δ : Type w} {m : Type w → Type w₂} [Monad m]
  (f : δ → (a : α) → β a → m δ) (init : δ) (t : Std.DTreeMap α β cmp) :
  m δ
Std.DTreeMap.foldlM.{u, v, w, w₂}
  {α : Type u} {β : α → Type v}
  {cmp : α → α → Ordering} {δ : Type w}
  {m : Type w → Type w₂} [Monad m]
  (f : δ → (a : α) → β a → m δ) (init : δ)
  (t : Std.DTreeMap α β cmp) : m δ

Folds the given monadic function over the mappings in the map in ascending order.

🔗def
Std.DTreeMap.forIn.{u, v, w, w₂} {α : Type u} {β : α → Type v}
  {cmp : α → α → Ordering} {δ : Type w} {m : Type w → Type w₂} [Monad m]
  (f : (a : α) → β a → δ → m (ForInStep δ)) (init : δ)
  (t : Std.DTreeMap α β cmp) : m δ
Std.DTreeMap.forIn.{u, v, w, w₂}
  {α : Type u} {β : α → Type v}
  {cmp : α → α → Ordering} {δ : Type w}
  {m : Type w → Type w₂} [Monad m]
  (f :
    (a : α) → β a → δ → m (ForInStep δ))
  (init : δ) (t : Std.DTreeMap α β cmp) :
  m δ

Support for the for loop construct in do blocks. Iteration happens in ascending order.

🔗def
Std.DTreeMap.forM.{u, v, w, w₂} {α : Type u} {β : α → Type v}
  {cmp : α → α → Ordering} {m : Type w → Type w₂} [Monad m]
  (f : (a : α) → β a → m PUnit) (t : Std.DTreeMap α β cmp) : m PUnit
Std.DTreeMap.forM.{u, v, w, w₂}
  {α : Type u} {β : α → Type v}
  {cmp : α → α → Ordering}
  {m : Type w → Type w₂} [Monad m]
  (f : (a : α) → β a → m PUnit)
  (t : Std.DTreeMap α β cmp) : m PUnit

Carries out a monadic action on each mapping in the tree map in ascending order.

20.19.9.6. 转换🔗

🔗def
Std.DTreeMap.ofList.{u, v} {α : Type u} {β : α → Type v}
  (l : List ((a : α) × β a))
  (cmp : α → α → Ordering := by exact compare) : Std.DTreeMap α β cmp
Std.DTreeMap.ofList.{u, v} {α : Type u}
  {β : α → Type v}
  (l : List ((a : α) × β a))
  (cmp : α → α → Ordering := by
    exact compare) :
  Std.DTreeMap α β cmp

Transforms a list of mappings into a tree map.

🔗def
Std.DTreeMap.toArray.{u, v} {α : Type u} {β : α → Type v}
  {cmp : α → α → Ordering} (t : Std.DTreeMap α β cmp) :
  Array ((a : α) × β a)
Std.DTreeMap.toArray.{u, v} {α : Type u}
  {β : α → Type v}
  {cmp : α → α → Ordering}
  (t : Std.DTreeMap α β cmp) :
  Array ((a : α) × β a)

Transforms the tree map into a list of mappings in ascending order.

🔗def
Std.DTreeMap.toList.{u, v} {α : Type u} {β : α → Type v}
  {cmp : α → α → Ordering} (t : Std.DTreeMap α β cmp) :
  List ((a : α) × β a)
Std.DTreeMap.toList.{u, v} {α : Type u}
  {β : α → Type v}
  {cmp : α → α → Ordering}
  (t : Std.DTreeMap α β cmp) :
  List ((a : α) × β a)

Transforms the tree map into a list of mappings in ascending order.

20.19.9.7. 非捆绑变体🔗

未捆绑的地图将格式良好的证明与数据分开。 这在定义 嵌套归纳类型 时主要有用。 要使用这些变体，请导入模块 Std.DTreeMap.Raw。

🔗structure
Std.DTreeMap.Raw.{u, v} (α : Type u) (β : α → Type v)
  (_cmp : α → α → Ordering := by exact compare) : Type (max u v)
Std.DTreeMap.Raw.{u, v} (α : Type u)
  (β : α → Type v)
  (_cmp : α → α → Ordering := by
    exact compare) :
  Type (max u v)

Dependent tree maps without a bundled well-formedness invariant, suitable for use in nested inductive types. The well-formedness invariant is called Raw.WF. When in doubt, prefer DTreeMap over DTreeMap.Raw. Lemmas about the operations on Std.DTreeMap.Raw are available in the module Std.Data.DTreeMap.Raw.Lemmas.

A tree map stores an assignment of keys to values. It depends on a comparator function that defines an ordering on the keys and provides efficient order-dependent queries, such as retrieval of the minimum or maximum.

To ensure that the operations behave as expected, the comparator function cmp should satisfy certain laws that ensure a consistent ordering:

  • If a is less than (or equal) to b, then b is greater than (or equal) to a and vice versa (see the OrientedCmp typeclass).

  • If a is less than or equal to b and b is, in turn, less than or equal to c, then a is less than or equal to c (see the TransCmp typeclass).

Keys for which cmp a b = Ordering.eq are considered the same, i.e., there can be only one entry with key either a or b in a tree map. Looking up either a or b always yields the same entry, if any is present. The get operations of the dependent tree map additionally require a LawfulEqCmp instance to ensure that cmp a b = .eq always implies a = b, so that their respective value types are equal.

To avoid expensive copies, users should make sure that the tree map is used linearly.

Internally, the tree maps are represented as size-bounded trees, a type of self-balancing binary search tree with efficient order statistic lookups.

Constructor

Std.DTreeMap.Raw.mk.{u, v}

Fields

inner : Std.DTreeMap.Internal.Impl α β

Internal implementation detail of the tree map.

🔗structure
Std.DTreeMap.Raw.WF.{u, v} {α : Type u} {β : α → Type v}
  {cmp : α → α → Ordering} (t : Std.DTreeMap.Raw α β cmp) : Prop
Std.DTreeMap.Raw.WF.{u, v} {α : Type u}
  {β : α → Type v}
  {cmp : α → α → Ordering}
  (t : Std.DTreeMap.Raw α β cmp) : Prop

Well-formedness predicate for tree maps. Users of DTreeMap will not need to interact with this. Users of DTreeMap.Raw will need to provide proofs of WF to lemmas and should use lemmas like WF.empty and WF.insert (which are always named exactly like the operations they are about) to show that map operations preserve well-formedness. The constructors of this type are internal implementation details and should not be accessed by users.

Constructor

Std.DTreeMap.Raw.WF.mk.{u, v}

Fields

out : t.inner.WF

Internal implementation detail of the tree map.

20.19.10. 基于树的集合🔗

🔗structure
Std.TreeSet.{u} (α : Type u)
  (cmp : α → α → Ordering := by exact compare) : Type u
Std.TreeSet.{u} (α : Type u)
  (cmp : α → α → Ordering := by
    exact compare) :
  Type u

Tree sets.

A tree set stores elements of a certain type in a certain order. It depends on a comparator function that defines an ordering on the keys and provides efficient order-dependent queries, such as retrieval of the minimum or maximum.

To ensure that the operations behave as expected, the comparator function cmp should satisfy certain laws that ensure a consistent ordering:

  • If a is less than (or equal) to b, then b is greater than (or equal) to a and vice versa (see the OrientedCmp typeclass).

  • If a is less than or equal to b and b is, in turn, less than or equal to c, then a is less than or equal to c (see the TransCmp typeclass).

Keys for which cmp a b = Ordering.eq are considered the same, i.e., there can be only one of them be contained in a single tree set at the same time.

To avoid expensive copies, users should make sure that the tree set is used linearly.

Internally, the tree sets are represented as size-bounded trees, a type of self-balancing binary search tree with efficient order statistic lookups.

For use in proofs, the type Std.ExtTreeSet of extensional tree sets should be preferred. This type comes with several extensionality lemmas and provides the same functions but requires a TransCmp instance to work with.

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

20.19.10.1. 创建🔗

🔗def
Std.TreeSet.empty.{u} {α : Type u} {cmp : α → α → Ordering} :
  Std.TreeSet α cmp
Std.TreeSet.empty.{u} {α : Type u}
  {cmp : α → α → Ordering} :
  Std.TreeSet α cmp

Creates a new empty tree set. It is also possible and recommended to use the empty collection notations ∅ and {} to create an empty tree set. simp replaces empty with ∅.

20.19.10.2. 特性🔗

🔗def
Std.TreeSet.isEmpty.{u} {α : Type u} {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp) : Bool
Std.TreeSet.isEmpty.{u} {α : Type u}
  {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp) : Bool

Returns true if the tree set contains no mappings.

🔗def
Std.TreeSet.size.{u} {α : Type u} {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp) : Nat
Std.TreeSet.size.{u} {α : Type u}
  {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp) : Nat

Returns the number of mappings present in the map.

20.19.10.3. 查询🔗

🔗def
Std.TreeSet.contains.{u} {α : Type u} {cmp : α → α → Ordering}
  (l : Std.TreeSet α cmp) (a : α) : Bool
Std.TreeSet.contains.{u} {α : Type u}
  {cmp : α → α → Ordering}
  (l : Std.TreeSet α cmp) (a : α) : Bool

Returns true if a, or an element equal to a according to the comparator cmp, is contained in the set. There is also a Prop-valued version of this: a ∈ t is equivalent to t.contains a = true.

Observe that this is different behavior than for lists: for lists, ∈ uses = and contains uses == for equality checks, while for tree sets, both use the given comparator cmp.

🔗def
Std.TreeSet.get.{u} {α : Type u} {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp) (a : α) (h : a ∈ t) : α
Std.TreeSet.get.{u} {α : Type u}
  {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp) (a : α)
  (h : a ∈ t) : α

Retrieves the key from the set that matches a. Ensures that such a key exists by requiring a proof of a ∈ m. The result is guaranteed to be pointer equal to the key in the set.

🔗def
Std.TreeSet.get!.{u} {α : Type u} {cmp : α → α → Ordering} [Inhabited α]
  (t : Std.TreeSet α cmp) (a : α) : α
Std.TreeSet.get!.{u} {α : Type u}
  {cmp : α → α → Ordering} [Inhabited α]
  (t : Std.TreeSet α cmp) (a : α) : α

Checks if given key is contained and returns the key if it is, otherwise panics. If no panic occurs the result is guaranteed to be pointer equal to the key in the set.

🔗def
Std.TreeSet.get?.{u} {α : Type u} {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp) (a : α) : Option α
Std.TreeSet.get?.{u} {α : Type u}
  {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp) (a : α) :
  Option α

Checks if given key is contained and returns the key if it is, otherwise none. The result in the some case is guaranteed to be pointer equal to the key in the map.

🔗def
Std.TreeSet.getD.{u} {α : Type u} {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp) (a fallback : α) : α
Std.TreeSet.getD.{u} {α : Type u}
  {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp)
  (a fallback : α) : α

Checks if given key is contained and returns the key if it is, otherwise fallback. If they key is contained the result is guaranteed to be pointer equal to the key in the set.

20.19.10.3.1. 基于排序的查询🔗

🔗def
Std.TreeSet.atIdx.{u} {α : Type u} {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp) (n : Nat) (h : n < t.size) : α
Std.TreeSet.atIdx.{u} {α : Type u}
  {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp) (n : Nat)
  (h : n < t.size) : α

Returns the n-th smallest element.

🔗def
Std.TreeSet.atIdx!.{u} {α : Type u} {cmp : α → α → Ordering}
  [Inhabited α] (t : Std.TreeSet α cmp) (n : Nat) : α
Std.TreeSet.atIdx!.{u} {α : Type u}
  {cmp : α → α → Ordering} [Inhabited α]
  (t : Std.TreeSet α cmp) (n : Nat) : α

Returns the n-th smallest element, or panics if n is at least t.size.

🔗def
Std.TreeSet.atIdx?.{u} {α : Type u} {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp) (n : Nat) : Option α
Std.TreeSet.atIdx?.{u} {α : Type u}
  {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp) (n : Nat) :
  Option α

Returns the n-th smallest element, or none if n is at least t.size.

🔗def
Std.TreeSet.atIdxD.{u} {α : Type u} {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp) (n : Nat) (fallback : α) : α
Std.TreeSet.atIdxD.{u} {α : Type u}
  {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp) (n : Nat)
  (fallback : α) : α

Returns the n-th smallest element, or fallback if n is at least t.size.

🔗def
Std.TreeSet.getGE.{u} {α : Type u} {cmp : α → α → Ordering}
  [Std.TransCmp cmp] (t : Std.TreeSet α cmp) (k : α)
  (h : ∃ a, a ∈ t ∧ (cmp a k).isGE = true) : α
Std.TreeSet.getGE.{u} {α : Type u}
  {cmp : α → α → Ordering}
  [Std.TransCmp cmp]
  (t : Std.TreeSet α cmp) (k : α)
  (h :
    ∃ a, a ∈ t ∧ (cmp a k).isGE = true) :
  α

Given a proof that such an element exists, retrieves the smallest element that is greater than or equal to the given element.

🔗def
Std.TreeSet.getGE!.{u} {α : Type u} {cmp : α → α → Ordering}
  [Inhabited α] (t : Std.TreeSet α cmp) (k : α) : α
Std.TreeSet.getGE!.{u} {α : Type u}
  {cmp : α → α → Ordering} [Inhabited α]
  (t : Std.TreeSet α cmp) (k : α) : α

Tries to retrieve the smallest element that is greater than or equal to the given element, panicking if no such element exists.

🔗def
Std.TreeSet.getGE?.{u} {α : Type u} {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp) (k : α) : Option α
Std.TreeSet.getGE?.{u} {α : Type u}
  {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp) (k : α) :
  Option α

Tries to retrieve the smallest element that is greater than or equal to the given element, returning none if no such element exists.

🔗def
Std.TreeSet.getGED.{u} {α : Type u} {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp) (k fallback : α) : α
Std.TreeSet.getGED.{u} {α : Type u}
  {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp)
  (k fallback : α) : α

Tries to retrieve the smallest element that is greater than or equal to the given element, returning fallback if no such element exists.

🔗def
Std.TreeSet.getGT.{u} {α : Type u} {cmp : α → α → Ordering}
  [Std.TransCmp cmp] (t : Std.TreeSet α cmp) (k : α)
  (h : ∃ a, a ∈ t ∧ cmp a k = Ordering.gt) : α
Std.TreeSet.getGT.{u} {α : Type u}
  {cmp : α → α → Ordering}
  [Std.TransCmp cmp]
  (t : Std.TreeSet α cmp) (k : α)
  (h :
    ∃ a, a ∈ t ∧ cmp a k = Ordering.gt) :
  α

Given a proof that such an element exists, retrieves the smallest element that is greater than the given element.

🔗def
Std.TreeSet.getGT!.{u} {α : Type u} {cmp : α → α → Ordering}
  [Inhabited α] (t : Std.TreeSet α cmp) (k : α) : α
Std.TreeSet.getGT!.{u} {α : Type u}
  {cmp : α → α → Ordering} [Inhabited α]
  (t : Std.TreeSet α cmp) (k : α) : α

Tries to retrieve the smallest element that is greater than the given element, panicking if no such element exists.

🔗def
Std.TreeSet.getGT?.{u} {α : Type u} {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp) (k : α) : Option α
Std.TreeSet.getGT?.{u} {α : Type u}
  {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp) (k : α) :
  Option α

Tries to retrieve the smallest element that is greater than the given element, returning none if no such element exists.

🔗def
Std.TreeSet.getGTD.{u} {α : Type u} {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp) (k fallback : α) : α
Std.TreeSet.getGTD.{u} {α : Type u}
  {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp)
  (k fallback : α) : α

Tries to retrieve the smallest element that is greater than the given element, returning fallback if no such element exists.

🔗def
Std.TreeSet.getLE.{u} {α : Type u} {cmp : α → α → Ordering}
  [Std.TransCmp cmp] (t : Std.TreeSet α cmp) (k : α)
  (h : ∃ a, a ∈ t ∧ (cmp a k).isLE = true) : α
Std.TreeSet.getLE.{u} {α : Type u}
  {cmp : α → α → Ordering}
  [Std.TransCmp cmp]
  (t : Std.TreeSet α cmp) (k : α)
  (h :
    ∃ a, a ∈ t ∧ (cmp a k).isLE = true) :
  α

Given a proof that such an element exists, retrieves the largest element that is less than or equal to the given element.

🔗def
Std.TreeSet.getLE!.{u} {α : Type u} {cmp : α → α → Ordering}
  [Inhabited α] (t : Std.TreeSet α cmp) (k : α) : α
Std.TreeSet.getLE!.{u} {α : Type u}
  {cmp : α → α → Ordering} [Inhabited α]
  (t : Std.TreeSet α cmp) (k : α) : α

Tries to retrieve the largest element that is less than or equal to the given element, panicking if no such element exists.

🔗def
Std.TreeSet.getLE?.{u} {α : Type u} {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp) (k : α) : Option α
Std.TreeSet.getLE?.{u} {α : Type u}
  {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp) (k : α) :
  Option α

Tries to retrieve the largest element that is less than or equal to the given element, returning none if no such element exists.

🔗def
Std.TreeSet.getLED.{u} {α : Type u} {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp) (k fallback : α) : α
Std.TreeSet.getLED.{u} {α : Type u}
  {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp)
  (k fallback : α) : α

Tries to retrieve the largest element that is less than or equal to the given element, returning fallback if no such element exists.

🔗def
Std.TreeSet.getLT.{u} {α : Type u} {cmp : α → α → Ordering}
  [Std.TransCmp cmp] (t : Std.TreeSet α cmp) (k : α)
  (h : ∃ a, a ∈ t ∧ cmp a k = Ordering.lt) : α
Std.TreeSet.getLT.{u} {α : Type u}
  {cmp : α → α → Ordering}
  [Std.TransCmp cmp]
  (t : Std.TreeSet α cmp) (k : α)
  (h :
    ∃ a, a ∈ t ∧ cmp a k = Ordering.lt) :
  α

Given a proof that such an element exists, retrieves the smallest element that is less than the given element.

🔗def
Std.TreeSet.getLT!.{u} {α : Type u} {cmp : α → α → Ordering}
  [Inhabited α] (t : Std.TreeSet α cmp) (k : α) : α
Std.TreeSet.getLT!.{u} {α : Type u}
  {cmp : α → α → Ordering} [Inhabited α]
  (t : Std.TreeSet α cmp) (k : α) : α

Tries to retrieve the smallest element that is less than the given element, panicking if no such element exists.

🔗def
Std.TreeSet.getLT?.{u} {α : Type u} {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp) (k : α) : Option α
Std.TreeSet.getLT?.{u} {α : Type u}
  {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp) (k : α) :
  Option α

Tries to retrieve the smallest element that is less than the given element, returning none if no such element exists.

🔗def
Std.TreeSet.getLTD.{u} {α : Type u} {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp) (k fallback : α) : α
Std.TreeSet.getLTD.{u} {α : Type u}
  {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp)
  (k fallback : α) : α

Tries to retrieve the smallest element that is less than the given element, returning fallback if no such element exists.

🔗def
Std.TreeSet.min.{u} {α : Type u} {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp) (h : t.isEmpty = false) : α
Std.TreeSet.min.{u} {α : Type u}
  {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp)
  (h : t.isEmpty = false) : α

Given a proof that the tree set is not empty, retrieves the smallest element.

🔗def
Std.TreeSet.min!.{u} {α : Type u} {cmp : α → α → Ordering} [Inhabited α]
  (t : Std.TreeSet α cmp) : α
Std.TreeSet.min!.{u} {α : Type u}
  {cmp : α → α → Ordering} [Inhabited α]
  (t : Std.TreeSet α cmp) : α

Tries to retrieve the smallest element of the tree set, panicking if the set is empty.

🔗def
Std.TreeSet.min?.{u} {α : Type u} {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp) : Option α
Std.TreeSet.min?.{u} {α : Type u}
  {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp) : Option α

Tries to retrieve the smallest element of the tree set, returning none if the set is empty.

🔗def
Std.TreeSet.minD.{u} {α : Type u} {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp) (fallback : α) : α
Std.TreeSet.minD.{u} {α : Type u}
  {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp) (fallback : α) :
  α

Tries to retrieve the smallest element of the tree set, returning fallback if the tree set is empty.

🔗def
Std.TreeSet.max.{u} {α : Type u} {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp) (h : t.isEmpty = false) : α
Std.TreeSet.max.{u} {α : Type u}
  {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp)
  (h : t.isEmpty = false) : α

Given a proof that the tree set is not empty, retrieves the largest element.

🔗def
Std.TreeSet.max!.{u} {α : Type u} {cmp : α → α → Ordering} [Inhabited α]
  (t : Std.TreeSet α cmp) : α
Std.TreeSet.max!.{u} {α : Type u}
  {cmp : α → α → Ordering} [Inhabited α]
  (t : Std.TreeSet α cmp) : α

Tries to retrieve the largest element of the tree set, panicking if the set is empty.

🔗def
Std.TreeSet.max?.{u} {α : Type u} {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp) : Option α
Std.TreeSet.max?.{u} {α : Type u}
  {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp) : Option α

Tries to retrieve the largest element of the tree set, returning none if the set is empty.

🔗def
Std.TreeSet.maxD.{u} {α : Type u} {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp) (fallback : α) : α
Std.TreeSet.maxD.{u} {α : Type u}
  {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp) (fallback : α) :
  α

Tries to retrieve the largest element of the tree set, returning fallback if the tree set is empty.

20.19.10.4. 修改🔗

🔗def
Std.TreeSet.insert.{u} {α : Type u} {cmp : α → α → Ordering}
  (l : Std.TreeSet α cmp) (a : α) : Std.TreeSet α cmp
Std.TreeSet.insert.{u} {α : Type u}
  {cmp : α → α → Ordering}
  (l : Std.TreeSet α cmp) (a : α) :
  Std.TreeSet α cmp

Inserts the given element into the set. If the tree set already contains an element that is equal (with regard to cmp) to the given element, then the tree set is returned unchanged.

Note: this non-replacement behavior is true for TreeSet and TreeSet.Raw. The insert function on TreeMap, DTreeMap, TreeMap.Raw and DTreeMap.Raw behaves differently: it will overwrite an existing mapping.

🔗def
Std.TreeSet.insertMany.{u, u_1} {α : Type u} {cmp : α → α → Ordering}
  {ρ : Type u_1} [ForIn Id ρ α] (t : Std.TreeSet α cmp) (l : ρ) :
  Std.TreeSet α cmp
Std.TreeSet.insertMany.{u, u_1}
  {α : Type u} {cmp : α → α → Ordering}
  {ρ : Type u_1} [ForIn Id ρ α]
  (t : Std.TreeSet α cmp) (l : ρ) :
  Std.TreeSet α cmp

Inserts multiple elements into the tree set by iterating over the given collection and calling insert. If the same element (with respect to cmp) appears multiple times, the first occurrence takes precedence.

Note: this precedence behavior is true for TreeSet and TreeSet.Raw. The insertMany function on TreeMap, DTreeMap, TreeMap.Raw and DTreeMap.Raw behaves differently: it will prefer the last appearance.

🔗def
Std.TreeSet.containsThenInsert.{u} {α : Type u} {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp) (a : α) : Bool × Std.TreeSet α cmp
Std.TreeSet.containsThenInsert.{u}
  {α : Type u} {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp) (a : α) :
  Bool × Std.TreeSet α cmp

Checks whether an element is present in a set and inserts the element if it was not found. If the tree set already contains an element that is equal (with regard to cmp to the given element, then the tree set is returned unchanged.

Equivalent to (but potentially faster than) calling contains followed by insert.

🔗def
Std.TreeSet.erase.{u} {α : Type u} {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp) (a : α) : Std.TreeSet α cmp
Std.TreeSet.erase.{u} {α : Type u}
  {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp) (a : α) :
  Std.TreeSet α cmp

Removes the given key if it exists.

🔗def
Std.TreeSet.eraseMany.{u, u_1} {α : Type u} {cmp : α → α → Ordering}
  {ρ : Type u_1} [ForIn Id ρ α] (t : Std.TreeSet α cmp) (l : ρ) :
  Std.TreeSet α cmp
Std.TreeSet.eraseMany.{u, u_1}
  {α : Type u} {cmp : α → α → Ordering}
  {ρ : Type u_1} [ForIn Id ρ α]
  (t : Std.TreeSet α cmp) (l : ρ) :
  Std.TreeSet α cmp

Erases multiple items from the tree set by iterating over the given collection and calling erase.

🔗def
Std.TreeSet.filter.{u} {α : Type u} {cmp : α → α → Ordering}
  (f : α → Bool) (m : Std.TreeSet α cmp) : Std.TreeSet α cmp
Std.TreeSet.filter.{u} {α : Type u}
  {cmp : α → α → Ordering} (f : α → Bool)
  (m : Std.TreeSet α cmp) :
  Std.TreeSet α cmp

Removes all elements from the tree set for which the given function returns false.

🔗def
Std.TreeSet.merge.{u} {α : Type u} {cmp : α → α → Ordering}
  (t₁ t₂ : Std.TreeSet α cmp) : Std.TreeSet α cmp
Std.TreeSet.merge.{u} {α : Type u}
  {cmp : α → α → Ordering}
  (t₁ t₂ : Std.TreeSet α cmp) :
  Std.TreeSet α cmp

Returns a set that contains all mappings of t₁ and `t₂.

This function ensures that t₁ is used linearly. Hence, as long as t₁ is unshared, the performance characteristics follow the following imperative description: Iterate over all mappings in t₂, inserting them into t₁.

Hence, the runtime of this method scales logarithmically in the size of t₁ and linearly in the size of t₂ as long as t₁ is unshared.

🔗def
Std.TreeSet.partition.{u} {α : Type u} {cmp : α → α → Ordering}
  (f : α → Bool) (t : Std.TreeSet α cmp) :
  Std.TreeSet α cmp × Std.TreeSet α cmp
Std.TreeSet.partition.{u} {α : Type u}
  {cmp : α → α → Ordering} (f : α → Bool)
  (t : Std.TreeSet α cmp) :
  Std.TreeSet α cmp × Std.TreeSet α cmp

Partitions a tree set into two tree sets based on a predicate.

20.19.10.5. 迭代🔗

🔗def
Std.TreeSet.iter.{u} {α : Type u} {cmp : α → α → Ordering}
  (m : Std.TreeSet α cmp) : Std.Iter α
Std.TreeSet.iter.{u} {α : Type u}
  {cmp : α → α → Ordering}
  (m : Std.TreeSet α cmp) : Std.Iter α

Returns a finite iterator over the entries of a tree set. The iterator yields the elements of the set in order and then terminates.

Termination properties:

  • Finite instance: always

  • Productive instance: always

🔗def
Std.TreeSet.all.{u} {α : Type u} {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp) (p : α → Bool) : Bool
Std.TreeSet.all.{u} {α : Type u}
  {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp) (p : α → Bool) :
  Bool

Check if any element satisfies the predicate, short-circuiting if a predicate succeeds.

🔗def
Std.TreeSet.any.{u} {α : Type u} {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp) (p : α → Bool) : Bool
Std.TreeSet.any.{u} {α : Type u}
  {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp) (p : α → Bool) :
  Bool

Check if all elements satisfy the predicate, short-circuiting if a predicate fails.

🔗def
Std.TreeSet.foldl.{u, w} {α : Type u} {cmp : α → α → Ordering}
  {δ : Type w} (f : δ → α → δ) (init : δ) (t : Std.TreeSet α cmp) : δ
Std.TreeSet.foldl.{u, w} {α : Type u}
  {cmp : α → α → Ordering} {δ : Type w}
  (f : δ → α → δ) (init : δ)
  (t : Std.TreeSet α cmp) : δ

Folds the given function over the elements of the tree set in ascending order.

🔗def
Std.TreeSet.foldlM.{u, u_1, u_2} {α : Type u} {cmp : α → α → Ordering}
  {m : Type u_1 → Type u_2} {δ : Type u_1} [Monad m] (f : δ → α → m δ)
  (init : δ) (t : Std.TreeSet α cmp) : m δ
Std.TreeSet.foldlM.{u, u_1, u_2}
  {α : Type u} {cmp : α → α → Ordering}
  {m : Type u_1 → Type u_2} {δ : Type u_1}
  [Monad m] (f : δ → α → m δ) (init : δ)
  (t : Std.TreeSet α cmp) : m δ

Monadically computes a value by folding the given function over the elements in the tree set in ascending order.

🔗def
Std.TreeSet.foldr.{u, w} {α : Type u} {cmp : α → α → Ordering}
  {δ : Type w} (f : α → δ → δ) (init : δ) (t : Std.TreeSet α cmp) : δ
Std.TreeSet.foldr.{u, w} {α : Type u}
  {cmp : α → α → Ordering} {δ : Type w}
  (f : α → δ → δ) (init : δ)
  (t : Std.TreeSet α cmp) : δ

Folds the given function over the elements of the tree set in descending order.

🔗def
Std.TreeSet.foldrM.{u, u_1, u_2} {α : Type u} {cmp : α → α → Ordering}
  {m : Type u_1 → Type u_2} {δ : Type u_1} [Monad m] (f : α → δ → m δ)
  (init : δ) (t : Std.TreeSet α cmp) : m δ
Std.TreeSet.foldrM.{u, u_1, u_2}
  {α : Type u} {cmp : α → α → Ordering}
  {m : Type u_1 → Type u_2} {δ : Type u_1}
  [Monad m] (f : α → δ → m δ) (init : δ)
  (t : Std.TreeSet α cmp) : m δ

Monadically computes a value by folding the given function over the elements in the tree set in descending order.

🔗def
Std.TreeSet.forIn.{u, w, w₂} {α : Type u} {cmp : α → α → Ordering}
  {δ : Type w} {m : Type w → Type w₂} [Monad m]
  (f : α → δ → m (ForInStep δ)) (init : δ) (t : Std.TreeSet α cmp) : m δ
Std.TreeSet.forIn.{u, w, w₂} {α : Type u}
  {cmp : α → α → Ordering} {δ : Type w}
  {m : Type w → Type w₂} [Monad m]
  (f : α → δ → m (ForInStep δ)) (init : δ)
  (t : Std.TreeSet α cmp) : m δ

Support for the for loop construct in do blocks. The iteration happens in ascending order.

🔗def
Std.TreeSet.forM.{u, w, w₂} {α : Type u} {cmp : α → α → Ordering}
  {m : Type w → Type w₂} [Monad m] (f : α → m PUnit)
  (t : Std.TreeSet α cmp) : m PUnit
Std.TreeSet.forM.{u, w, w₂} {α : Type u}
  {cmp : α → α → Ordering}
  {m : Type w → Type w₂} [Monad m]
  (f : α → m PUnit)
  (t : Std.TreeSet α cmp) : m PUnit

Carries out a monadic action on each element in the tree set in ascending order.

20.19.10.6. 转换🔗

🔗def
Std.TreeSet.toList.{u} {α : Type u} {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp) : List α
Std.TreeSet.toList.{u} {α : Type u}
  {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp) : List α

Transforms the tree set into a list of elements in ascending order.

🔗def
Std.TreeSet.ofList.{u} {α : Type u} (l : List α)
  (cmp : α → α → Ordering := by exact compare) : Std.TreeSet α cmp
Std.TreeSet.ofList.{u} {α : Type u}
  (l : List α)
  (cmp : α → α → Ordering := by
    exact compare) :
  Std.TreeSet α cmp

Transforms a list into a tree set.

🔗def
Std.TreeSet.toArray.{u} {α : Type u} {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp) : Array α
Std.TreeSet.toArray.{u} {α : Type u}
  {cmp : α → α → Ordering}
  (t : Std.TreeSet α cmp) : Array α

Transforms the tree set into an array of elements in ascending order.

🔗def
Std.TreeSet.ofArray.{u} {α : Type u} (a : Array α)
  (cmp : α → α → Ordering := by exact compare) : Std.TreeSet α cmp
Std.TreeSet.ofArray.{u} {α : Type u}
  (a : Array α)
  (cmp : α → α → Ordering := by
    exact compare) :
  Std.TreeSet α cmp

Transforms an array into a tree set.

20.19.10.6.1. 非捆绑变体🔗

非捆绑集将格式良好的证明与数据分开。 这在定义 嵌套归纳类型 时主要有用。 要使用这些变体，请导入模块 Std.TreeSet.Raw。

🔗structure
Std.TreeSet.Raw.{u} (α : Type u)
  (cmp : α → α → Ordering := by exact compare) : Type u
Std.TreeSet.Raw.{u} (α : Type u)
  (cmp : α → α → Ordering := by
    exact compare) :
  Type u

Tree sets without a bundled well-formedness invariant, suitable for use in nested inductive types. The well-formedness invariant is called Raw.WF. When in doubt, prefer TreeSet over TreeSet.Raw. Lemmas about the operations on Std.TreeSet.Raw are available in the module Std.Data.TreeSet.Raw.Lemmas.

A tree set stores elements of a certain type in a certain order. It depends on a comparator function that defines an ordering on the keys and provides efficient order-dependent queries, such as retrieval of the minimum or maximum.

To ensure that the operations behave as expected, the comparator function cmp should satisfy certain laws that ensure a consistent ordering:

  • If a is less than (or equal) to b, then b is greater than (or equal) to a and vice versa (see the OrientedCmp typeclass).

  • If a is less than or equal to b and b is, in turn, less than or equal to c, then a is less than or equal to c (see the TransCmp typeclass).

Keys for which cmp a b = Ordering.eq are considered the same, i.e only one of them can be contained in a single tree set at the same time.

To avoid expensive copies, users should make sure that the tree set is used linearly.

Internally, the tree sets are represented as size-bounded trees, a type of self-balancing binary search tree with efficient order statistic lookups.

Constructor

Std.TreeSet.Raw.mk.{u}

Fields

inner : Std.TreeMap.Raw α Unit cmp

Internal implementation detail of the tree set.

🔗structure
Std.TreeSet.Raw.WF.{u} {α : Type u} {cmp : α → α → Ordering}
  (t : Std.TreeSet.Raw α cmp) : Prop
Std.TreeSet.Raw.WF.{u} {α : Type u}
  {cmp : α → α → Ordering}
  (t : Std.TreeSet.Raw α cmp) : Prop

Well-formedness predicate for tree sets. Users of TreeSet will not need to interact with this. Users of TreeSet.Raw will need to provide proofs of WF to lemmas and should use lemmas like WF.empty and WF.insert (which are always named exactly like the operations they are about) to show that set operations preserve well-formedness. The constructors of this type are internal implementation details and should not be accessed by users.

Constructor

Std.TreeSet.Raw.WF.mk.{u}

Fields

out : t.inner.WF

Internal implementation detail of the tree map.