20.19. 映射与集合🔗

映射是一种将键关联到值的数据结构。它们也常被称为字典、关联数组，或直接称为哈希表。

在 Lean 中，映射可能具有下列性质：

表示: 映射在内存中的表示可以是树，也可以是哈希表。当数据结构的引用被共享时，基于树的表示更合适，因为哈希表建立在数组之上。当引用不是唯一时，修改数组需要整体复制；而修改树时，只需复制从树根到被修改节点的路径。相比之下，当引用不共享时，哈希表可能更高效，因为未共享的数组可以在常数时间内原地修改。此外，基于树的映射会按顺序存储数据，因此支持按序遍历。
外延性: 映射可以看作从键到值的偏函数。 外延映射 指的是命题相等恰好符合这一解释的映射。这会让推理更加方便，但也会排除一些原本能够区分它们的有用操作。一般来说，只有在验证需要时才应使用外延映射。
是否依值: 依值映射 指的是其中每个值的类型由其对应的键决定，而不是保持常量的映射。依值映射具有更强的表达能力，但也更难使用。它们会对使用者提出更多要求。例如，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 标准库中，这些数据结构表示为“底层数据”与“其良构性证明”的一对值。这一点大多只是内部实现细节；不过，在一种情况下它与用户相关：这种表示方式会阻止它们被用在嵌套归纳类型中。

为了让它们能够用于嵌套归纳类型，标准库为每个容器都提供了“原始”变体，以及将其不变量分离出来的“分离式”版本。它们遵循如下命名约定：

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 是相应的数据结构）。

当映射或集合内部出现嵌套归纳类型时，应分三个阶段来定义：

先定义该嵌套归纳类型的原始版本，使其使用映射或集合类型的原始版本，并定义所有必要操作。
接着定义一个归纳谓词，断言原始嵌套类型中的所有映射或集合都是良构的，并证明原始类型上的操作保持良构性。
最后为该嵌套归纳类型构造合适的接口：定义一个 API，在需要时证明良构性性质，并把这些证明细节对用户隐藏起来。

使用 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) := bydescription:String⊢ (base description).WF
  constructoradescription:String⊢ ∀ (dir : String) (v : RawMaze), ∅[dir]? = some v → v.WFadescription:String⊢ ∅.WF
  .adescription:String⊢ ∀ (dir : String) (v : RawMaze), ∅[dir]? = some v → v.WF intro v h h'adescription:Stringv:Stringh:RawMazeh':∅[v]? = some h⊢ h.WF
    simp [Std.HashMap.Raw.getElem?_empty] at *All goals completed! 🐙
  .adescription:String⊢ ∅.WF exact HashMap.Raw.WF.emptyAll goals completed! 🐙

Definition `RawMaze.insert_wf` is a proposition; use `theorem` instead of `def`

Note: This linter can be disabled with `set_option linter.defProp false`def RawMaze.insert_wf (maze : RawMaze) :
    WF maze → WF next → WF (maze.insert dir next) := bynext:RawMazedir:Stringmaze:RawMaze⊢ maze.WF → next.WF → (maze.insert dir next).WF
  let ⟨desc, passages⟩ := mazenext:RawMazedir:Stringmaze:RawMazedesc:Stringpassages:HashMap.Raw String RawMaze⊢ { description := desc, passages := passages }.WF →
  next.WF → ({ description := desc, passages := passages }.insert dir next).WF
  intro ⟨wfMore, wfPassages⟩ wfNextnext: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
  constructoranext: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.WFanext: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
  .anext: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 intro dir' vanext: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
    rw [HashMap.Raw.getElem?_insert wfPassagesanext: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]anext: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
    splita.isTruenext: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.WFa.isFalsenext: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 <;>a.isTruenext: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.WFa.isFalsenext: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 introsa.isFalsenext: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 <;>a.isTruenext: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.WFa.isFalsenext: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 simp_all [wfMore dir']All goals completed! 🐙
  .anext: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 simp_all [HashMap.Raw.WF.insert]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 := bydescription:String⊢ (RawMaze.base description).WF apply RawMaze.base_wfAll 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' <| bymaze:Mazedir:Stringm':RawMazeh:maze.raw.passages[dir]? = some m'⊢ m'.WF
      let ⟨r, wf⟩ := mazemaze:Mazedir:Stringm':RawMazer:RawMazewf:r.WFh:{ raw := r, wf := wf }.raw.passages[dir]? = some m'⊢ m'.WF
      let ⟨wfAll, _⟩ := wfmaze: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
      apply wfAll dirmaze: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'
      apply hAll goals completed! 🐙

在线查看 ↪

20.19.1.3. 保持唯一引用的合适运算🔗

在使用数据结构时，应尽量确保尽可能多的引用保持唯一；这能让 Lean 在维持纯函数接口的同时，在幕后使用破坏性更新。映射与集合库提供了一些可用于保持引用唯一性的运算。特别是，在可能的情况下，应优先使用 alter 或 modify 之类的操作，而不是显式取出某个值、修改它、再将其重新插入。这些操作可以避免在修改过程中产生该值的第二个引用。

修改映射中的值

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)

在线查看 ↪

20.19.2. 哈希映射🔗

本节中的声明应通过 import Std.HashMap 导入。

结构体

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)

哈希映射。

这是一个简单的分离链接哈希表。哈希映射的数据由缓存的大小和桶数组组成，其中每个桶是键值对的链表。桶的数量始终是2的幂。哈希映射在插入元素时将其大小加倍，使得元素数量超过桶数量的 75%。

该哈希表由 Array 作为后备存储。用户应确保线性使用哈希映射以避免昂贵的复制。

哈希映射使用 ==（由 BEq 类型类提供）来比较键，并使用 hash（由 Hashable 类型类提供）来对它们进行哈希处理。为了确保操作按预期运行，== 应该是等价关系，而 a == b 应该蕴含 hash a = hash b（另请参见 EquivBEq 和 LawfulHashable 类型类）。如果 BEq 实例合法，即如果 a == b 蕴含 a = b，这两个条件都是自动的。

这些哈希映射包含内置的良构不变量，这意味着它们不能在嵌套归纳类型中使用。对于这些用例，Std.Data.HashMap.Raw 和 Std.Data.HashMap.Raw.WF 将不变量与哈希映射分开。如有疑问，请优先选择 HashMap 而不是 HashMap.Raw。

依值哈希映射（其中键可能出现在其值的类型中）可用作 Std.Data.DHashMap。

20.19.2.1. 创建🔗

定义

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 α β

创建一个新的空哈希映射。可以提供可选参数 capacity 来预先调整映射大小，以便它可以容纳给定数量的映射而无需重新分配。还可以使用空集合符号 ∅ 和 {} 来创建具有默认容量的空哈希映射。

20.19.2.2. 性质🔗

定义

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

哈希映射中存在的映射数量

定义

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

如果哈希映射不包含映射，则返回 true。

请注意，如果您的 BEq 实例不是自反的，或者您的 Hashable 实例不合法，则该函数有可能返回 false，即使不可能从哈希映射中获取任何内容。

结构体

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

当且仅当所有键和值都相等时，两个哈希映射在 Equiv 意义上是等效的。

构造子

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

字段

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

哈希映射的内部实现细节。

语法等价

关系 HashMap.Equiv 也可以写成一个中缀运算符，该运算符的作用域限定在其命名空间内：

term ::= ...
    | term ~m term

20.19.2.3. 查询🔗

定义

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

如果给定键存在映射，则返回 true。还有一个 Prop 值的版本：a ∈ m 相当于 m.contains a = true。

请注意，这与列表的行为不同：对于列表，∈ 使用 = 和 contains 使用 == 进行比较，而对于哈希映射，两者都使用 ==。

定义

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) : β

符号 m[a] 或 m[a]'h 优于直接调用此函数。

检索给定键的映射。通过要求 a ∈ m 的证明来确保此类映射的存在。

定义

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 : α) : β

符号 m[a]! 优于直接调用此函数。

尝试检索给定键的映射，如果不存在此类映射，则会触发 panic。

定义

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 β

符号 m[a]? 优于直接调用此函数。

尝试检索给定键的映射，如果不存在此类映射，则返回 none。

定义

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 : β) : β

尝试检索给定键的映射，如果不存在此类映射，则返回 fallback。

定义

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) : α

从映射中检索与 a 匹配的键。通过要求 a ∈ m 的证明来确保此类映射的存在。结果保证是等于映射中的键的指针。

定义

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 : α) : α

检查给定键的映射是否存在，如果存在则返回该键，否则会触发 panic。如果未触发 panic，结果保证是等于映射中的键的指针。

定义

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 α

检查给定键的映射是否存在，如果存在则返回该键，否则返回 none。 some 情况下的结果保证是等于映射中的键的指针。

定义

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 : α) : α

检查给定键的映射是否存在，如果存在则返回该键，否则返回 fallback。如果存在映射，则保证结果是等于映射中键的指针。

定义

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 α

按某种顺序返回哈希映射中存在的所有键的列表。

定义

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 α

按某种顺序返回哈希映射中存在的所有键的数组。

定义

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 β

按某种顺序返回哈希映射中存在的所有值的列表。

定义

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 β

按某种顺序返回哈希映射中存在的所有值的数组。

20.19.2.4. 修改🔗

定义

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 α β

就地修改与给定键关联的值，允许通过 Option 值替换函数创建新值和删除值。

此函数可确保线性使用该值。

定义

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 α β

就地修改与给定键关联的值。

此函数可确保线性使用该值。

定义

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 α β

检查映射中是否存在某个键，并无条件插入该键的值。

相当于（但可能比）调用 contains 后跟 insert 更快。

定义

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 α β

检查映射中是否存在某个键，如果未找到，则为该键插入一个值。

如果返回的 Bool 是 true，则返回的映射不变。如果 Bool 是 false，则返回的映射已插入新值。

相当于（但可能比）调用 contains 后跟 insertIfNew 更快。

定义

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 α β

删除给定键的映射（如果存在）。

定义

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 α β

删除给定函数返回 false 的哈希映射的所有映射。

定义

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 α γ

通过将给定函数应用于所有映射来更新哈希映射的值，仅保留函数返回 some 值的那些映射。

定义

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 α β

将给定的映射插入到映射中。如果给定键已经存在映射，则键和值都将被替换。

注意：此替换行为适用于 HashMap、DHashMap、HashMap.Raw 和 DHashMap.Raw。 insert 函数在 HashSet 和 HashSet.Raw 上的行为不同：如果匹配的键已存在，它将返回未更改的集合。

定义

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 α β

如果给定键没有映射，则将给定映射插入到映射中。否则，返回未更改的映射。

定义

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 α β

检查映射中是否存在某个键，返回关联的值，如果未找到，则为该键插入一个值。

如果返回值为 some v，则返回的映射不变。如果是 none，则返回的映射已插入新值。

相当于（但可能比）调用 get? 后跟 insertIfNew 更快。

定义

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 α β

通过迭代给定集合并调用 insert，将多个映射插入哈希映射。如果同一键出现多次，则最后一次出现的键优先。

注意：此优先行为适用于 HashMap、DHashMap、HashMap.Raw 和 DHashMap.Raw。 insertMany 函数在 HashSet 和 HashSet.Raw 上的行为不同：它会更喜欢第一次出现。

定义

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

将多个值为 () 的键插入哈希映射：为此迭代给定集合并调用 insertIfNew。如果同一个键出现多次，则第一次出现的键优先。

这主要用于实现 HashSet.insertMany，因此如果您正在考虑使用它，HashSet 或 HashSet.Raw 可能更适合您。

定义

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 α β

根据谓词将哈希映射划分为两个哈希映射。

定义

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 α β

计算给定哈希映射的并集。如果一个键同时出现在两个映射中，则第二个参数中包含的条目将出现在结果中。

该函数始终将较小的映射合并到较大的映射中，因此预期运行时间为 O(min(m₁.size, m₂.size))。

20.19.2.5. 迭代🔗

定义

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 (α × β)

返回哈希映射条目上的有限迭代器。迭代器按顺序生成映射的元素，然后终止。

终止性质：

Finite 实例：始终存在
Productive 实例：始终存在

定义

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 α

返回哈希映射条目上的有限迭代器。迭代器按顺序生成映射的元素，然后终止。

终止性质：

Finite 实例：始终存在
Productive 实例：始终存在

定义

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 β

返回哈希映射条目上的有限迭代器。迭代器按顺序生成映射的元素，然后终止。

终止性质：

Finite 实例：始终存在
Productive 实例：始终存在

定义

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 α γ

通过将给定函数应用于所有映射来更新哈希映射的值。

定义

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 α β) : γ

按某种顺序将给定函数折叠到哈希映射中的映射上。

定义

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 γ

通过按某种顺序将给定函数折叠到哈希映射中的映射来单子地计算值。

定义

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 γ

支持 for 循环在 do 块中的构造形式。

定义

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

按某种顺序对哈希映射中的每个映射执行单子操作。

20.19.2.6. 转换🔗

定义

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 α β

从映射列表创建哈希映射。如果同一键出现多次，则最后一次出现的键优先。

定义

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 (α × β)

按某种顺序将哈希映射转换为映射数组。

定义

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 (α × β)

将哈希映射按某种顺序转换为映射列表。

定义

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

从键数组创建哈希映射，将值 () 与每个键相关联。

这主要用于实现 HashSet.ofArray，因此如果您正在考虑使用它，HashSet 或 HashSet.Raw 可能更适合您。

定义

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

从键列表创建哈希映射，将值 () 与每个键相关联。

这主要用于实现 HashSet.ofList，因此如果您正在考虑使用它，HashSet 或 HashSet.Raw 可能更适合您。

20.19.2.7. 分离式变体🔗

分离式映射会将良构性证明与数据本身分开。这主要在定义嵌套归纳类型时有用。要使用这些变体，请导入模块 Std.HashMap.Raw 与 Std.HashMap.RawLemmas。

结构体

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)

没有内置的良构不变量的哈希映射，适合在嵌套归纳类型中使用。良构的不变量称为 Raw.WF。如有疑问，请优先选择 HashMap 而不是 HashMap.Raw。关于 Std.Data.HashMap.Raw 操作的引理可在模块 Std.Data.HashMap.RawLemmas 中找到。

该哈希表由 Array 作为后备存储。用户应确保线性使用哈希映射以避免昂贵的复制。

依值哈希映射（其中键可能出现在其值的类型中）可用作 Std.Data.Raw.DHashMap。

构造子

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

字段

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

哈希映射的内部实现细节。

结构体

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

哈希映射的良构谓词。 HashMap 的用户不需要与之交互。 HashMap.Raw 的用户需要向引理提供 WF 的证明，并且应该使用引理 WF.empty 和 WF.insert（它们的命名始终与它们所涉及的操作完全相同）来表明映射操作保持良构。

构造子

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

字段

out : m.inner.WF

哈希映射的内部实现细节。

20.19.3. 依值哈希映射🔗

本节中的声明应通过 import Std.DHashMap 导入。

结构体

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)

依值哈希映射。

该哈希表由 Array 作为后备存储。用户应确保线性使用哈希映射以避免昂贵的复制。

这些哈希映射包含内置的良构不变量，这意味着它们不能在嵌套归纳类型中使用。对于这些用例，Std.DHashMap.Raw 和 Std.DHashMap.Raw.WF 将不变量与哈希映射分开。如有疑问，请优先选择 DHashMap 而不是 DHashMap.Raw。

对于由于外延性而更方便在证明中使用的变体，请参阅 Std.ExtDHashMap，它定义于模块 Std.Data.ExtDHashMap。

20.19.3.1. 创建🔗

定义

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 α β

20.19.3.2. 性质🔗

定义

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

哈希映射中存在的映射数量

定义

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

如果哈希映射不包含映射，则返回 true。

请注意，如果您的 BEq 实例不是自反的，或者您的 Hashable 实例不合法，则该函数有可能返回 false，即使不可能从哈希映射中获取任何内容。

结构体

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

当且仅当所有键和值都相等时，两个哈希映射在 Equiv 意义上是等效的。

构造子

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

字段

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

哈希映射的内部实现细节。

语法等价

关系 DHashMap.Equiv 也可以写成一个中缀运算符，该运算符的作用域限定在其命名空间内：

term ::= ...
    | term ~m term

20.19.3.3. 查询🔗

定义

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

如果给定键存在映射，则返回 true。还有一个 Prop 值的版本：a ∈ m 相当于 m.contains a = true。

请注意，这与列表的行为不同：对于列表，∈ 使用 = 和 contains 使用 == 进行比较，而对于哈希映射，两者都使用 ==。

定义

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

检索给定键的映射。通过要求 a ∈ m 的证明来确保此类映射的存在。

使用 LawfulBEq 实例将检索到的值转换为正确的类型。

定义

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

尝试检索给定键的映射，如果不存在此类映射，则会触发 panic。

使用 LawfulBEq 实例将检索到的值转换为正确的类型。

定义

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)

尝试检索给定键的映射，如果不存在此类映射，则返回 none。

使用 LawfulBEq 实例将检索到的值转换为正确的类型。

定义

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

尝试检索给定键的映射，如果不存在此类映射，则返回 fallback。

使用 LawfulBEq 实例将检索到的值转换为正确的类型。

定义

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) : α

从映射中检索与 a 匹配的键。通过要求 a ∈ m 的证明来确保此类映射的存在。结果保证是等于映射中的键的指针。

定义

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 : α) : α

检查给定键的映射是否存在，如果存在则返回该键，否则会触发 panic。如果未触发 panic，结果保证是等于映射中的键的指针。

定义

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 α

检查给定键的映射是否存在，如果存在则返回该键，否则返回 none。 some 情况下的结果保证是等于映射中的键的指针。

定义

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 : α) : α

检查给定键的映射是否存在，如果存在则返回该键，否则返回 fallback。如果存在映射，则保证结果是等于映射中键的指针。

定义

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 α

按某种顺序返回哈希映射中存在的所有键的列表。

定义

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 α

按某种顺序返回哈希映射中存在的所有键的数组。

定义

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 β

按某种顺序返回哈希映射中存在的所有值的列表。

定义

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 β

按某种顺序返回哈希映射中存在的所有值的数组。

20.19.3.4. 修改🔗

定义

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 α β

就地修改与给定键关联的值，允许通过 Option 值替换函数创建新值和删除值。

此函数可确保线性使用该值。

定义

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 α β

就地修改与给定键关联的值。

此函数可确保线性使用该值。

定义

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 α β

检查映射中是否存在某个键，并无条件插入该键的值。

相当于（但可能比）调用 contains 后跟 insert 更快。

定义

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 α β

检查映射中是否存在某个键，如果未找到，则为该键插入一个值。

如果返回的 Bool 是 true，则返回的映射不变。如果 Bool 是 false，则返回的映射已插入新值。

相当于（但可能比）调用 contains 后跟 insertIfNew 更快。

定义

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 α β

删除给定键的映射（如果存在）。

定义

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 α β

删除给定函数返回 false 的哈希映射的所有映射。

定义

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 α δ

通过将给定函数应用于所有映射来更新哈希映射的值，仅保留函数返回 some 值的那些映射。

定义

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 α β

将给定的映射插入到映射中。如果给定键已经存在映射，则键和值都将被替换。

定义

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 α β

如果给定键没有映射，则将给定映射插入到映射中。否则，返回未更改的映射。

定义

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 α β

检查映射中是否存在某个键，返回关联的值，如果未找到，则为该键插入一个值。

如果返回值为 some v，则返回的映射不变。如果是 none，则返回的映射已插入新值。

相当于（但可能比）调用 get? 后跟 insertIfNew 更快。

使用 LawfulBEq 实例将检索到的值转换为正确的类型。

定义

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 α β

通过迭代给定集合并调用 insert，将多个映射插入哈希映射。如果同一键出现多次，则最后一次出现的键优先。

注意：此优先行为适用于 HashMap、DHashMap、HashMap.Raw 和 DHashMap.Raw。 insertMany 函数在 HashSet 和 HashSet.Raw 上的行为不同：它会更喜欢第一次出现。

定义

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 α β

根据谓词将哈希映射划分为两个哈希映射。

定义

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 α β

计算给定哈希映射的并集。如果一个键同时出现在两个映射中，则第二个参数中包含的条目将出现在结果中。

该函数始终将较小的映射合并到较大的映射中，因此预期运行时间为 O(min(m₁.size, m₂.size))。

20.19.3.5. 迭代🔗

定义

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)

返回依值哈希映射条目上的有限迭代器。迭代器按顺序生成映射的元素，然后终止。

终止性质：

Finite 实例：始终存在
Productive 实例：始终存在

定义

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 α

返回依值哈希映射的键上的有限迭代器。迭代器按顺序生成键，然后终止。

键和值类型必须位于同一个宇宙中。

终止性质：

Finite 实例：始终存在
Productive 实例：始终存在

定义

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 β

返回哈希映射值的有限迭代器。迭代器按顺序产生值，然后终止。

键和值类型必须位于同一个宇宙中。

终止性质：

Finite 实例：始终存在
Productive 实例：始终存在

定义

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 α δ

通过将给定函数应用于所有映射来更新哈希映射的值。

定义

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 α β) : δ

按某种顺序将给定函数折叠到哈希映射中的映射上。

定义

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 δ

通过按某种顺序将给定函数折叠到哈希映射中的映射来单子地计算值。

定义

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 δ

支持 for 循环在 do 块中的构造形式。

定义

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

按某种顺序对哈希映射中的每个映射执行单子操作。

20.19.3.6. 转换🔗

定义

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 α β

从映射列表创建哈希映射。如果同一键出现多次，则最后一次出现的键优先。

定义

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)

按某种顺序将哈希映射转换为映射数组。

定义

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)

将哈希映射按某种顺序转换为映射列表。

20.19.3.7. 分离式变体🔗

分离式映射会将良构性证明与数据本身分开。这主要在定义嵌套归纳类型时有用。要使用这些变体，请导入模块 Std.DHashMap.Raw 与 Std.DHashMap.RawLemmas。

结构体

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)

没有内置的良构不变量的依值哈希映射，适合在嵌套归纳类型中使用。良构的不变量称为 Raw.WF。如有疑问，请优先选择 DHashMap 而不是 DHashMap.Raw。关于 Std.Data.DHashMap.Raw 操作的引理可在模块 Std.Data.DHashMap.RawLemmas 中找到。

该哈希表由 Array 作为后备存储。用户应确保线性使用哈希映射以避免昂贵的复制。

构造子

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

字段

size : Nat

哈希映射中的映射数量。

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

哈希映射的内部实现细节。

归纳谓词

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

哈希映射的良构谓词。 DHashMap 的用户不需要与之交互。 DHashMap.Raw 的用户需要向引理提供 WF 的证明，并且应该使用像 WF.empty 和 WF.insert 这样的引理（它们的命名总是与它们所涉及的操作完全相同）来表明映射操作保持良构。该类型的构造函数是内部实现细节，用户不应访问。

构造子

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

哈希映射的内部实现细节。

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

哈希映射的内部实现细节。

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

哈希映射的内部实现细节。

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

哈希映射的内部实现细节。

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

哈希映射的内部实现细节。

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

哈希映射的内部实现细节。

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

哈希映射的内部实现细节。

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

哈希映射的内部实现细节。

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

哈希映射的内部实现细节。

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

哈希映射的内部实现细节。

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

哈希映射的内部实现细节。

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

哈希映射的内部实现细节。

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

哈希映射的内部实现细节。

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

哈希映射的内部实现细节。

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

哈希映射的内部实现细节。

20.19.4. 外延哈希映射🔗

本节中的声明应通过 import Std.ExtHashMap 导入。

结构体

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)

哈希映射。

该哈希表由 Array 作为后备存储。用户应确保线性使用哈希映射以避免昂贵的复制。

与常规哈希映射相比，Std.ExtHashMap 提供了多个外延引理，因此具有更多关于哈希映射相等性的引理。然而，这也使其失去了自由迭代哈希映射的能力。

这些哈希映射包含内置的良构不变量，这意味着它们不能在嵌套归纳类型中使用。对于这些用例，Std.HashMap.Raw 和 Std.HashMap.Raw.WF 将不变量与哈希映射分开。如有疑问，请优先选择 HashMap 或 ExtHashMap 而不是 HashMap.Raw。

依值哈希映射（其中键可能出现在其值的类型中）以 Std.ExtDHashMap 形式提供，定义于模块 Std.Data.ExtDHashMap。

20.19.4.1. 创建🔗

定义

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 α β

20.19.4.2. 性质🔗

定义

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

哈希映射中存在的映射数量

定义

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

如果哈希映射不包含映射，则返回 true。

请注意，如果您的 BEq 实例不是自反的，或者您的 Hashable 实例不合法，则该函数有可能返回 false，即使不可能从哈希映射中获取任何内容。

20.19.4.3. 查询🔗

定义

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

如果给定键存在映射，则返回 true。还有一个 Prop 值的版本：a ∈ m 相当于 m.contains a = true。

请注意，这与列表的行为不同：对于列表，∈ 使用 = 和 contains 使用 == 进行比较，而对于哈希映射，两者都使用 ==。

定义

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) : β

符号 m[a] 或 m[a]'h 优于直接调用此函数。

检索给定键的映射。通过要求 a ∈ m 的证明来确保此类映射的存在。

定义

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 : α) : β

符号 m[a]! 优于直接调用此函数。

尝试检索给定键的映射，如果不存在此类映射，则会触发 panic。

定义

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 β

符号 m[a]? 优于直接调用此函数。

尝试检索给定键的映射，如果不存在此类映射，则返回 none。

定义

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 : β) : β

尝试检索给定键的映射，如果不存在此类映射，则返回 fallback。

定义

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) : α

从映射中检索与 a 匹配的键。通过要求 a ∈ m 的证明来确保此类映射的存在。结果保证是等于映射中的键的指针。

定义

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 : α) : α

检查给定键的映射是否存在，如果存在则返回该键，否则会触发 panic。如果未触发 panic，结果保证是等于映射中的键的指针。

定义

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 α

检查给定键的映射是否存在，如果存在则返回该键，否则返回 none。 some 情况下的结果保证是等于映射中的键的指针。

定义

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 : α) : α

检查给定键的映射是否存在，如果存在则返回该键，否则返回 fallback。如果存在映射，则保证结果是等于映射中键的指针。

20.19.4.4. 修改🔗

定义

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 α β

就地修改与给定键关联的值，允许通过 Option 值替换函数创建新值和删除值。

此函数可确保线性使用该值。

定义

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 α β

就地修改与给定键关联的值。

此函数可确保线性使用该值。

定义

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 α β

检查映射中是否存在某个键，并无条件插入该键的值。

相当于（但可能比）调用 contains 后跟 insert 更快。

定义

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 α β

检查映射中是否存在某个键，如果未找到，则为该键插入一个值。

如果返回的 Bool 是 true，则返回的映射不变。如果 Bool 是 false，则返回的映射已插入新值。

相当于（但可能比）调用 contains 后跟 insertIfNew 更快。

定义

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 α β

删除给定键的映射（如果存在）。

定义

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 α β

删除给定函数返回 false 的哈希映射的所有映射。

定义

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 α γ

通过将给定函数应用于所有映射来更新哈希映射的值，仅保留函数返回 some 值的那些映射。

定义

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 α β

将给定的映射插入到映射中。如果给定键已经存在映射，则键和值都将被替换。

定义

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 α β

如果给定键没有映射，则将给定映射插入到映射中。否则，返回未更改的映射。

定义

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 α β

检查映射中是否存在某个键，返回关联的值，如果未找到，则为该键插入一个值。

如果返回值为 some v，则返回的映射不变。如果是 none，则返回的映射已插入新值。

相当于（但可能比）调用 get? 后跟 insertIfNew 更快。

定义

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 α β

通过迭代给定集合并调用 insert，将多个映射插入哈希映射。如果同一键出现多次，则最后一次出现的键优先。

注意：此优先行为适用于 HashMap、DHashMap、HashMap.Raw 和 DHashMap.Raw。 insertMany 函数在 HashSet 和 HashSet.Raw 上的行为不同：它会更喜欢第一次出现。

定义

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

将多个值为 () 的键插入哈希映射：为此迭代给定集合并调用 insertIfNew。如果同一个键出现多次，则第一次出现的键优先。

这主要用于实现 HashSet.insertMany，因此如果您正在考虑使用它，HashSet 或 HashSet.Raw 可能更适合您。

20.19.4.5. 迭代🔗

定义

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 α γ

通过将给定函数应用于所有映射来更新哈希映射的值。

20.19.4.6. 转换🔗

定义

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 α β

从映射列表创建哈希映射。如果同一键出现多次，则最后一次出现的键优先。

定义

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

从键数组创建哈希映射，将值 () 与每个键相关联。

这主要用于实现 HashSet.ofArray，因此如果您正在考虑使用它，HashSet 或 HashSet.Raw 可能更适合您。

定义

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

从键列表创建哈希映射，将值 () 与每个键相关联。

这主要用于实现 HashSet.ofList，因此如果您正在考虑使用它，HashSet 或 HashSet.Raw 可能更适合您。

20.19.5. 外延依值哈希映射🔗

本节中的声明应通过 import Std.ExtDHashMap 导入。

结构体

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)

外延依值哈希映射。

该哈希表由 Array 作为后备存储。用户应确保线性使用哈希映射以避免昂贵的复制。

哈希映射使用 ==（由 BEq 类型类提供）来比较键，并使用 hash（由 Hashable 类型类提供）来对它们进行哈希处理。为了确保操作按预期运行，== 必须是等价关系，并且 a == b 必须隐含 hash a = hash b（另请参见 EquivBEq 和 LawfulHashable 类型类）。如果 BEq 实例合法，即如果 a == b 蕴含 a = b，这两个条件都是自动的。

与常规依值哈希映射相比，Std.ExtDHashMap 提供了多个外延引理，因此具有更多关于哈希映射相等性的引理。然而，这也使其失去了自由迭代哈希映射的能力。

20.19.5.1. 创建🔗

定义

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 α β

20.19.5.2. 性质🔗

定义

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

哈希映射中存在的映射数量

定义

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

如果哈希映射不包含映射，则返回 true。

请注意，如果您的 BEq 实例不是自反的，或者您的 Hashable 实例不合法，则该函数有可能返回 false，即使不可能从哈希映射中获取任何内容。

20.19.5.3. 查询🔗

定义

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

如果给定键存在映射，则返回 true。还有一个 Prop 值的版本：a ∈ m 相当于 m.contains a = true。

请注意，这与列表的行为不同：对于列表，∈ 使用 = 和 contains 使用 == 进行比较，而对于哈希映射，两者都使用 ==。

定义

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

检索给定键的映射。通过要求 a ∈ m 的证明来确保此类映射的存在。

使用 LawfulBEq 实例将检索到的值转换为正确的类型。

定义

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

尝试检索给定键的映射，如果不存在此类映射，则会触发 panic。

使用 LawfulBEq 实例将检索到的值转换为正确的类型。

定义

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)

尝试检索给定键的映射，如果不存在此类映射，则返回 none。

使用 LawfulBEq 实例将检索到的值转换为正确的类型。

定义

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

尝试检索给定键的映射，如果不存在此类映射，则返回 fallback。

使用 LawfulBEq 实例将检索到的值转换为正确的类型。

定义

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) : α

从映射中检索与 a 匹配的键。通过要求 a ∈ m 的证明来确保此类映射的存在。结果保证是等于映射中的键的指针。

定义

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 : α) : α

检查给定键的映射是否存在，如果存在则返回该键，否则会触发 panic。如果未触发 panic，结果保证是等于映射中的键的指针。

定义

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 α

检查给定键的映射是否存在，如果存在则返回该键，否则返回 none。 some 情况下的结果保证是等于映射中的键的指针。

定义

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 : α) : α

检查给定键的映射是否存在，如果存在则返回该键，否则返回 fallback。如果存在映射，则保证结果是等于映射中键的指针。

20.19.5.4. 修改🔗

定义

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 α β

就地修改与给定键关联的值，允许通过 Option 值替换函数创建新值和删除值。

此函数可确保线性使用该值。

定义

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 α β

就地修改与给定键关联的值。

此函数可确保线性使用该值。

定义

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 α β

检查映射中是否存在某个键，并无条件插入该键的值。

相当于（但可能比）调用 contains 后跟 insert 更快。

定义

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 α β

检查映射中是否存在某个键，如果未找到，则为该键插入一个值。

如果返回的 Bool 是 true，则返回的映射不变。如果 Bool 是 false，则返回的映射已插入新值。

相当于（但可能比）调用 contains 后跟 insertIfNew 更快。

定义

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 α β

删除给定键的映射（如果存在）。

定义

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 α β

删除给定函数返回 false 的哈希映射的所有映射。

定义

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 α γ

通过将给定函数应用于所有映射来更新哈希映射的值，仅保留函数返回 some 值的那些映射。

定义

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 α β

将给定的映射插入到映射中。如果给定键已经存在映射，则键和值都将被替换。

定义

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 α β

如果给定键没有映射，则将给定映射插入到映射中。否则，返回未更改的映射。

定义

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 α β

检查映射中是否存在某个键，返回关联的值，如果未找到，则为该键插入一个值。

如果返回值为 some v，则返回的映射不变。如果是 none，则返回的映射已插入新值。

相当于（但可能比）调用 get? 后跟 insertIfNew 更快。

使用 LawfulBEq 实例将检索到的值转换为正确的类型。

定义

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 α β

通过迭代给定集合并调用 insert，将多个映射插入哈希映射。如果同一键出现多次，则最后一次出现的键优先。

注意：此优先行为适用于 HashMap、DHashMap、HashMap.Raw 和 DHashMap.Raw。 insertMany 函数在 HashSet 和 HashSet.Raw 上的行为不同：它会更喜欢第一次出现。

20.19.5.5. 迭代🔗

定义

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 α γ

通过将给定函数应用于所有映射来更新哈希映射的值。

20.19.5.6. 转换🔗

定义

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 α β

从映射列表创建哈希映射。如果同一键出现多次，则最后一次出现的键优先。

20.19.6. 哈希集合🔗

结构体

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

哈希集。

这是一个简单的分离链接哈希表。哈希集的数据由缓存大小和桶数组组成，其中每个桶是键的链表。桶的数量始终是2的幂。插入元素后，哈希集的大小会加倍，使得元素数量超过桶数量的 75%。

该哈希表由 Array 作为后备存储。用户应确保哈希集是线性使用的，以避免昂贵的复制。

哈希集使用 ==（由 BEq 类型类提供）来比较元素，并使用 hash（由 Hashable 类型类提供）对它们进行哈希处理。为了确保操作按预期运行，== 应该是等价关系，而 a == b 应该蕴含 hash a = hash b（另请参见 EquivBEq 和 LawfulHashable 类型类）。如果 BEq 实例合法，即如果 a == b 蕴含 a = b，这两个条件都是自动的。

这些哈希集包含内置的良构不变量，这意味着它们不能在嵌套归纳类型中使用。对于这些用例，Std.Data.HashSet.Raw 和 Std.Data.HashSet.Raw.WF 将不变量与哈希集分开。如有疑问，请优先选择 HashSet 而不是 HashSet.Raw。

构造子

Std.HashSet.mk.{u}

字段

inner : Std.HashMap α Unit

哈希集合的内部实现细节。

20.19.6.1. 创建🔗

定义

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 α

创建一个新的空哈希集。可以提供可选参数 capacity 来预先调整集合的大小，以便它可以容纳给定数量的元素而无需重新分配。还可以使用空集合符号 ∅ 和 {} 创建具有默认容量的空哈希集。

20.19.6.2. 性质🔗

定义

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

如果哈希集不包含元素，则返回 true。

请注意，如果您的 BEq 实例不是自反的，或者您的 Hashable 实例不合法，则该函数有可能返回 false，即使 m.contains a = false 对所有 a 都成立。

定义

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

集合中存在的元素数量

结构体

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

两个哈希集在 Equiv 意义上是等效的，当且仅当它们的所有值都相等。

构造子

Std.HashSet.Equiv.mk.{u}

字段

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

哈希映射的内部实现细节。

语法等价

关系 HashSet.Equiv 也可以写成一个中缀运算符，该运算符的作用域限定在其命名空间内：

term ::= ...
    | term ~m term

20.19.6.3. 查询🔗

定义

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

如果给定的键存在于集合中，则返回 true。还有一个 Prop 值的版本：a ∈ m 相当于 m.contains a = true。

请注意，这与列表的行为不同：对于列表，∈ 使用 = 和 contains 使用 == 进行比较，而对于哈希集，两者都使用 ==。

定义

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) : α

从匹配 a 的集合中检索键。通过要求 a ∈ m 的证明来确保这样的键存在。结果保证是等于集合中的键的指针。

定义

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 : α) : α

检查是否包含给定的键，如果包含则返回该键，否则会触发 panic。如果未触发 panic，则结果保证是等于集合中的键的指针。

定义

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 α

检查是否包含给定的键，如果包含则返回该键，否则返回 none。 some 情况下的结果保证是等于集合中的键的指针。

定义

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 : α) : α

检查是否包含给定的键，如果包含则返回该键，否则返回 fallback。如果包含它们的键，则保证结果是等于集合中的键的指针。

20.19.6.4. 修改🔗

定义

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 α

将给定元素插入集合中。如果哈希集已包含与给定元素相等（关于 ==）的元素，则哈希集将原样返回。

注意：这种非替换行为对于 HashSet 和 HashSet.Raw 来说是正确的。 insert 函数在 HashMap、DHashMap、HashMap.Raw 和 DHashMap.Raw 上的行为不同：它将改写现有映射。

定义

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 α

通过迭代给定集合并调用 insert，将多个映射插入到哈希集中。如果同一个键出现多次，则第一次出现的键优先。

注意：此优先行为适用于 HashSet 和 HashSet.Raw。 insertMany 函数在 HashMap、DHashMap、HashMap.Raw 和 DHashMap.Raw 上的行为有所不同：它会优先采用最后一次出现。

定义

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 α

删除该元素（如果存在）。

定义

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 α

从哈希集中删除给定函数返回 false 的所有元素。

定义

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 α

检查集合中是否存在某个元素，如果未找到则插入该元素。如果哈希集已包含与给定元素相等（关于 ==）的元素，则哈希集将原样返回。

相当于（但可能比）调用 contains 后跟 insert 更快。

定义

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 α

根据谓词将哈希集划分为两个哈希集。

定义

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 α

计算给定哈希集的并集。

此函数始终将较小的集合合并到较大的集合中，因此预期运行时间为 O(min(m₁.size, m₂.size))。

20.19.6.5. 迭代🔗

定义

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 α

返回哈希集元素的有限迭代器。迭代器按顺序产生集合的元素，然后终止。

终止性质：

Finite 实例：始终存在
Productive 实例：始终存在

定义

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

检查是否所有元素都满足谓词，如果谓词失败则短路。

定义

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

检查是否有任何元素满足谓词，如果谓词成功则短路。

定义

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 α) : β

按某种顺序将给定函数折叠到哈希集的元素上。

定义

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 β

通过按某种顺序将给定函数折叠到哈希集中的元素上，单子地计算一个值。

定义

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 β

支持 for 循环在 do 块中的构造形式。

定义

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

按某种顺序对哈希集中的每个元素执行单子操作。

20.19.6.6. 转换🔗

定义

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

从元素列表创建哈希集。请注意，与重复调用 insert 不同，如果集合包含多个相等的元素（对于 ==），则集合中的最后一个元素将出现在返回的哈希集中。

定义

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 α

将哈希集按某种顺序转换为元素列表。

定义

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

从元素数组创建哈希集。请注意，与重复调用 insert 不同，如果集合包含多个相等的元素（对于 ==），则集合中的最后一个元素将出现在返回的哈希集中。

定义

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 α

将哈希集按某种顺序转换为元素数组。

20.19.6.7. 分离式变体🔗

分离式集合会将良构性证明与数据本身分开。这主要在定义嵌套归纳类型时有用。要使用这些变体，请导入模块 Std.HashSet.Raw 与 Std.HashSet.RawLemmas。

结构体

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

没有内置的良构不变量的哈希集，适合在嵌套归纳类型中使用。良构的不变量称为 Raw.WF。如有疑问，请优先选择 HashSet 而不是 HashSet.Raw。关于 Std.Data.HashSet.Raw 操作的引理可在模块 Std.Data.HashSet.RawLemmas 中找到。

该哈希表由 Array 作为后备存储。用户应确保哈希集是线性使用的，以避免昂贵的复制。

构造子

Std.HashSet.Raw.mk.{u}

字段

inner : Std.HashMap.Raw α Unit

哈希集合的内部实现细节。

结构体

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

哈希集的良构谓词。 HashSet 的用户不需要与之交互。 HashSet.Raw 的用户需要向引理提供 WF 的证明，并且应该使用像 WF.empty 和 WF.insert 这样的引理（它们的命名总是与它们所涉及的操作完全相同）来表明集合操作保持良构。

构造子

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

字段

out : m.inner.WF

哈希集合的内部实现细节。

20.19.7. 外延哈希集合🔗

结构体

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

哈希集。

该哈希表由 Array 作为后备存储。用户应确保哈希集是线性使用的，以避免昂贵的复制。

与常规哈希集相比，Std.ExtHashSet 提供了多个外延引理，因此具有更多关于哈希映射相等性的引理。然而，这也使其失去了自由迭代哈希集的能力。

这些哈希集包含内置的良构不变量，这意味着它们不能在嵌套归纳类型中使用。对于这些用例，Std.HashSet.Raw 和 Std.HashSet.Raw.WF 将不变量与哈希集分开。如有疑问，请优先选择 HashSet 或 ExtHashSet 而不是 HashSet.Raw。

构造子

Std.ExtHashSet.mk.{u}

字段

inner : Std.ExtHashMap α Unit

哈希集合的内部实现细节。

20.19.7.1. 创建🔗

定义

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 α

20.19.7.2. 性质🔗

定义

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

如果哈希集不包含元素，则返回 true。

请注意，如果您的 BEq 实例不是自反的，或者您的 Hashable 实例不合法，则该函数有可能返回 false，即使 m.contains a = false 对所有 a 都成立。

定义

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

集合中存在的元素数量

20.19.7.3. 查询🔗

定义

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

如果给定的键存在于集合中，则返回 true。还有一个 Prop 值的版本：a ∈ m 相当于 m.contains a = true。

请注意，这与列表的行为不同：对于列表，∈ 使用 = 和 contains 使用 == 进行比较，而对于哈希集，两者都使用 ==。

定义

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) : α

从匹配 a 的集合中检索键。通过要求 a ∈ m 的证明来确保这样的键存在。结果保证是等于集合中的键的指针。

定义

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 : α) : α

检查是否包含给定的键，如果包含则返回该键，否则会触发 panic。如果未触发 panic，则结果保证是等于集合中的键的指针。

定义

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 α

检查是否包含给定的键，如果包含则返回该键，否则返回 none。 some 情况下的结果保证是等于集合中的键的指针。

定义

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 : α) : α

检查是否包含给定的键，如果包含则返回该键，否则返回 fallback。如果包含它们的键，则保证结果是等于集合中的键的指针。

20.19.7.4. 修改🔗

定义

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 α

将给定元素插入集合中。如果哈希集已包含与给定元素相等（关于 ==）的元素，则哈希集将原样返回。

注意：这种非替换行为对于 ExtHashSet 和 ExtHashSet.Raw 来说是正确的。 insert 函数在 ExtHashMap、DExtHashMap、ExtHashMap.Raw 和 DExtHashMap.Raw 上的行为不同：它将改写现有映射。

定义

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 α

通过迭代给定集合并调用 insert，将多个映射插入到哈希集中。如果同一个键出现多次，则第一次出现的键优先。

注意：此优先行为适用于 ExtHashSet 和 ExtHashSet.Raw。 insertMany 函数在 ExtHashMap、DExtHashMap、ExtHashMap.Raw 和 DExtHashMap.Raw 上的行为有所不同：它会优先采用最后一次出现。

定义

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 α

删除该元素（如果存在）。

定义

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 α

从哈希集中删除给定函数返回 false 的所有元素。

定义

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 α

检查集合中是否存在某个元素，如果未找到则插入该元素。如果哈希集已包含与给定元素相等（关于 ==）的元素，则哈希集将原样返回。

相当于（但可能比）调用 contains 后跟 insert 更快。

20.19.7.5. 转换🔗

定义

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

定义

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

20.19.8. 基于树的映射🔗

本节中的声明应通过 import Std.TreeMap 导入。

结构体

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)

树映射。

树映射存储键到值的对应关系。它依赖一个比较器函数来定义键的顺序，并提供高效的顺序相关查询，例如检索最小值或最大值。

为确保各项操作符合预期，比较器函数 cmp 应满足若干保证顺序一致的定律：

如果 a 小于（或等于）b，那么 b 大于（或等于）a，反之亦然（参见 OrientedCmp 类型类）。
如果 a 小于或等于 b，而 b 又小于或等于 c，那么 a 小于或等于 c（参见 TransCmp 类型类）。

满足 cmp a b = Ordering.eq 的键被视为相同；也就是说，树映射中只能有一个键为 a 或 b 的条目。查找 a 或 b 总会得到同一个条目（如果存在）。

为避免高昂的复制开销，用户应确保以线性方式使用树映射。

树映射在内部表示为带大小界限的树，这是一类支持高效顺序统计查询的自平衡二叉搜索树。

在证明中，最好使用外延树映射类型 Std.ExtTreeMap。该类型带有多个外延性引理并提供相同的函数，但需要 TransCmp 实例才能使用。

这些树映射内置了良构性不变量，因此不能用于嵌套归纳类型。在这种场景中，Std.TreeMap.Raw 和 Std.TreeMap.Raw.WF 将该不变量与树映射分离。若不确定，请优先使用 TreeMap 而非 TreeMap.Raw。

20.19.8.1. 创建🔗

定义

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

创建一个新的空树映射。也可以并且推荐使用空集合记法 ∅ 和 {} 来创建空树映射。simp 会将 empty 替换为 ∅。

20.19.8.2. 性质🔗

定义

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

返回映射中现有对应关系的数量。

定义

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

如果树映射不含任何对应关系，则返回 true。

20.19.8.3. 查询🔗

定义

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

如果树映射不含任何对应关系，则返回 true；这里的对应关系可以属于给定键 a，也可以属于依比较器判断为与 a 相等的键。比较器为 cmp。它还有一个取值为 Prop 的版本：a ∈ t 等价于 t.contains a = true。

请注意，这与列表的行为不同：对于列表，∈ 使用 = 检查相等性，而 contains 使用 ==；对于树映射，两者都使用给定的比较器 cmp。

定义

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) : β

给定“给定键的对应关系存在”的证明，检索该键对应的值。

使用 LawfulEqCmp 实例将检索到的值转换为正确的类型。

定义

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 : α) : β

尝试检索给定键对应的值；如果不存在这样的对应关系，则触发 panic。

使用 LawfulEqCmp 实例将检索到的值转换为正确的类型。

定义

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 β

尝试检索给定键对应的值；如果不存在这样的对应关系，则返回 none。

使用 LawfulEqCmp 实例将检索到的值转换为正确的类型。

定义

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 : β) : β

尝试检索给定键对应的值；如果不存在这样的对应关系，则返回 fallback。

使用 LawfulEqCmp 实例将检索到的值转换为正确的类型。

定义

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) : α

从与 a 匹配的对应关系中检索键。它要求提供 a ∈ m 的证明，以保证这样的对应关系存在。结果保证与映射中的键指针相等。

定义

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 : α) : α

检查给定键的对应关系是否存在；若存在则返回该键，否则触发 panic。如果未触发 panic，则结果保证与映射中的键指针相等。

定义

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 α

检查给定键的对应关系是否存在；若存在则返回该键，否则返回 none。在结果为 some 时，其中的键保证与映射中的键指针相等。

定义

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 : α) : α

检查给定键的对应关系是否存在；若存在则返回该键，否则返回 fallback。如果对应关系存在，则结果保证与映射中的键指针相等。

定义

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 α

按升序返回树映射中所有键的列表。

定义

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 α

按升序返回树映射中所有键的数组。

定义

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 β

按键的升序返回树映射中所有值的列表。

定义

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 β

按键的升序返回树映射中所有值的数组。

20.19.8.3.1. 基于顺序的查询🔗

定义

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) : α × β

返回键为第 n 小的键值对。

定义

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) :
  α × β

返回键为第 n 小的键值对；如果 n 不小于 t.size，则触发 panic。

定义

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 (α × β)

返回键为第 n 小的键值对；若无此结果则返回 none，具体而言，是在 n 不小于 t.size 时。

定义

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 : α × β) : α × β

返回键为第 n 小的键值对；若无此结果则返回 fallback，具体而言，是在 n 不小于 t.size 时。

定义

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) :
  α × β

给定“存在这样的对应关系”的证明，检索最小且大于或等于给定键的键值对。

定义

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 : α) :
  α × β

尝试检索最小且大于或等于给定键的键值对；如果不存在，则触发 panic。

定义

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 (α × β)

尝试检索最小且大于或等于给定键的键值对；如果不存在，则返回 none。

定义

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 : α × β) : α × β

尝试检索最小且大于或等于给定键的键值对；如果不存在，则返回 fallback。

定义

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) :
  α × β

给定“存在这样的对应关系”的证明，检索最小且大于给定键的键值对。

定义

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 : α) :
  α × β

尝试检索最小且大于给定键的键值对；如果不存在，则触发 panic。

定义

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 (α × β)

尝试检索最小且大于给定键的键值对；如果不存在，则返回 none。

定义

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 : α × β) : α × β

尝试检索最小且大于给定键的键值对；如果不存在，则返回 fallback。

定义

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) :
  α × β

给定“存在这样的对应关系”的证明，检索最大且小于或等于给定键的键值对。

定义

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 : α) :
  α × β

尝试检索最大且小于或等于给定键的键值对；如果不存在，则触发 panic。

定义

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 (α × β)

尝试检索最大且小于或等于给定键的键值对；如果不存在，则返回 none。

定义

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 : α × β) : α × β

尝试检索最大且小于或等于给定键的键值对；如果不存在，则返回 fallback。

定义

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) :
  α × β

给定“存在这样的对应关系”的证明，检索最大且小于给定键的键值对。

定义

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 : α) :
  α × β

尝试检索最大且小于给定键的键值对；如果不存在，则触发 panic。

定义

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 (α × β)

尝试检索最大且小于给定键的键值对；如果不存在，则返回 none。

定义

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 : α × β) : α × β

尝试检索最大且小于给定键的键值对；如果不存在，则返回 fallback。

定义

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) :
  α

给定“存在这样的对应关系”的证明，检索最小且大于或等于给定键的键。

定义

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 : α) : α

尝试检索最小且大于或等于给定键的键；如果不存在，则触发 panic。

定义

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 α

尝试检索最小且大于或等于给定键的键；如果不存在，则返回 none。

定义

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 : α) : α

尝试检索最小且大于或等于给定键的键；如果不存在，则返回 fallback。

定义

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) :
  α

给定“存在这样的对应关系”的证明，检索最小且大于给定键的键。

定义

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 : α) : α

尝试检索最小且大于给定键的键；如果不存在，则触发 panic。

定义

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 α

尝试检索最小且大于给定键的键；如果不存在，则返回 none。

定义

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 : α) : α

尝试检索最小且大于给定键的键；如果不存在，则返回 fallback。

定义

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) :
  α

给定“存在这样的对应关系”的证明，检索最大且小于或等于给定键的键。

定义

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 : α) : α

尝试检索最大且小于或等于给定键的键；如果不存在，则触发 panic。

定义

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 α

尝试检索最大且小于或等于给定键的键；如果不存在，则返回 none。

定义

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 : α) : α

尝试检索最大且小于或等于给定键的键；如果不存在，则返回 fallback。

定义

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) :
  α

给定“存在这样的对应关系”的证明，检索最大且小于给定键的键。

定义

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 : α) : α

尝试检索最大且小于给定键的键；如果不存在，则触发 panic。

定义

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 α

尝试检索最大且小于给定键的键；如果不存在，则返回 none。

定义

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 : α) : α

尝试检索最大且小于给定键的键；如果不存在，则返回 fallback。

定义

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) : α

返回第 n 小的键。

定义

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) : α

返回第 n 小的键；如果 n 不小于 t.size，则触发 panic。

定义

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 α

返回第 n 小的键；若无此结果则返回 none，具体而言，是在 n 不小于 t.size 时。

定义

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 : α) : α

返回第 n 小的键；若无此结果则返回 fallback，具体而言，是在 n 不小于 t.size 时。

定义

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) : α × β

给定树映射非空的证明，检索键最小的键值对。

定义

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) : α × β

尝试检索树映射中键最小的键值对；如果映射为空，则触发 panic。

定义

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 (α × β)

尝试检索树映射中键最小的键值对；如果映射为空，则返回 none。

定义

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 : α × β) : α × β

尝试检索树映射中键最小的键值对；如果映射为空，则返回 fallback。

定义

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) : α

给定树映射非空的证明，检索最小的键。

定义

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) : α

尝试检索树映射中最小的键；如果映射为空，则触发 panic。

定义

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 α

尝试检索树映射中最小的键；如果映射为空，则返回 none。

定义

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 : α) : α

尝试检索树映射中最小的键；如果映射为空，则返回 fallback。

定义

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) : α × β

给定树映射非空的证明，检索键最大的键值对。

定义

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) : α × β

尝试检索树映射中键最大的键值对；如果映射为空，则触发 panic。

定义

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 (α × β)

尝试检索树映射中键最大的键值对；如果映射为空，则返回 none。

定义

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 : α × β) : α × β

尝试检索树映射中键最大的键值对；如果映射为空，则返回 fallback。

定义

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) : α

给定树映射非空的证明，检索最大的键。

定义

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) : α

尝试检索树映射中最大的键；如果映射为空，则触发 panic。

定义

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 α

尝试检索树映射中最大的键；如果映射为空，则返回 none。

定义

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 : α) : α

尝试检索树映射中最大的键；如果映射为空，则返回 fallback。

20.19.8.4. 修改🔗

定义

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

原地修改与给定键关联的值，并允许通过一个返回 Option 的替换函数创建或删除值。

此函数确保以线性方式使用该值。

定义

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

原地修改与给定键关联的值。

此函数确保以线性方式使用该值。

定义

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

检查映射中是否存在某个键，并无条件插入该键对应的值。

等价于（但可能快于）依次调用 contains 和 insert。

定义

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

检查映射中是否存在某个键；如果未找到，则插入该键对应的值。如果返回的 Bool 为 true，返回的映射不变。如果 Bool 为 false，则返回的映射中已插入新值。

等价于（但可能快于）依次调用 contains 和 insertIfNew。

定义

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

如果给定键的对应关系存在，则将其移除。

定义

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

迭代给定集合并调用 erase，从树映射中删除多个对应关系。

定义

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

移除映射中所有使给定函数返回 false 的对应关系。

定义

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

将给定函数应用于所有对应关系以更新映射中的值，仅保留函数返回 some 值的对应关系。

定义

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

将给定的对应关系插入映射。如果给定键已有对应关系，则键和值都会被替换。

定义

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

如果给定键没有对应关系，则将给定的对应关系插入映射；否则原样返回映射。

定义

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

检查映射中是否存在某个键并返回关联的值；如果未找到，则插入该键对应的值。

如果返回值为 some v，则返回的映射不变。如果返回值为 none，则返回的映射中已插入新值。

等价于（但可能快于）依次调用 get? 和 insertIfNew。

使用 LawfulEqCmp 实例将检索到的值转换为正确的类型。

定义

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

迭代给定集合并调用 insert，将多个对应关系插入树映射。如果同一个键出现多次，则以最后一次出现为准。

注意：TreeMap、DTreeMap、TreeMap.Raw 和 DTreeMap.Raw 都采用这种优先规则。insertMany 函数在 TreeSet 和 TreeSet.Raw 上的行为不同：它优先保留第一次出现的元素。

定义

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

迭代给定集合并调用 insertIfNew，将多个元素插入树映射。如果同一个键出现多次，则以第一次出现为准。

定义

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

返回包含 t₁ 和 t₂ 中所有对应关系的映射。如果两个映射含有同一个键 k（按 cmp 判断），则使用给定函数，根据 t₁ 和 t₂ 中各自的值确定新值。

此函数确保以线性方式使用 t₁。如果合并函数也以线性方式使用 t₁ 中各个值，即以线性方式使用第二个参数（第一个类型为 β a 的参数），则这些值同样只被线性使用。因此，只要 t₁ 未被共享，其性能特征可用以下命令式过程描述：迭代 t₂ 中的所有对应关系；若 t₁ 尚不包含冲突的对应关系，就将其插入 t₁；若 t₁ 已含冲突的对应关系，则使用给定的合并函数，将 t₂ 中的对应关系合并到 t₁ 的对应关系中。最后返回 t₁。

因此，此方法的运行时间关于 t₁ 的大小呈对数增长，关于 t₂ 的大小呈线性增长，只要 t₁ 未被共享。

定义

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

依据谓词将一个树映射分割为两个树映射。

20.19.8.5. 迭代🔗

定义

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 (α × β)

返回遍历树映射条目的有限迭代器。迭代器按顺序产出映射中的元素，然后终止。

终止性质：

Finite 实例：始终成立
Productive 实例：始终成立

定义

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 α

返回遍历树映射键的有限迭代器。迭代器按顺序产出键，然后终止。

键类型和值类型必须位于同一个宇宙中。

终止性质：

Finite 实例：始终成立
Productive 实例：始终成立

定义

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 β

返回遍历树映射值的有限迭代器。迭代器按顺序产出值，然后终止。

键类型和值类型必须位于同一个宇宙中。

终止性质：

Finite 实例：始终成立
Productive 实例：始终成立

定义

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

将给定函数应用于所有对应关系，以更新映射中的值。

定义

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

检查是否所有元素都满足谓词；一旦谓词不成立便短路。

定义

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

检查是否有任一元素满足谓词；一旦谓词不成立便短路。

定义

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) : δ

按升序用给定函数折叠映射中的对应关系。

定义

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 δ

按升序用给定的单子函数折叠映射中的对应关系。

定义

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) : δ

按降序用给定函数折叠映射中的对应关系。

定义

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 δ

按降序用给定的单子函数折叠映射中的对应关系。

定义

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 δ

为 for 循环构造在 do 块中使用提供支持。迭代按升序进行。

定义

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

按升序对树映射中的每个对应关系执行单子动作。

20.19.8.6. 转换🔗

定义

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

将对应关系列表转换为树映射。

定义

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 (α × β)

按升序将树映射转换为对应关系列表。

定义

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

将对应关系列表转换为树映射。

定义

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 (α × β)

按升序将树映射转换为对应关系列表。

定义

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

将键数组转换为树映射。

定义

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

将键列表转换为树映射。

20.19.8.6.1. 分离式变体🔗

分离式映射会将良构性证明与数据本身分开。这主要在定义嵌套归纳类型时有用。要使用这些变体，请导入模块 Std.TreeMap.Raw。

结构体

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)

不内置良构性不变量的树映射，适用于嵌套归纳类型。其良构性不变量称为 Raw.WF。若不确定，请优先使用 TreeMap 而非 TreeMap.Raw。关于 Std.TreeMap.Raw 各项操作的引理可在模块 Std.Data.TreeMap.Raw.Lemmas 中找到。

树映射存储键到值的对应关系。它依赖一个比较器函数来定义键的顺序，并提供高效的顺序相关查询，例如检索最小值或最大值。

为确保各项操作符合预期，比较器函数 cmp 应满足若干保证顺序一致的定律：

如果 a 小于（或等于）b，那么 b 大于（或等于）a，反之亦然（参见 OrientedCmp 类型类）。
如果 a 小于或等于 b，而 b 又小于或等于 c，那么 a 小于或等于 c（参见 TransCmp 类型类）。

满足 cmp a b = Ordering.eq 的键被视为相同；也就是说，树映射中只能有一个键为 a 或 b 的条目。查找 a 或 b 总会得到同一个条目（如果存在）。

为避免高昂的复制开销，用户应确保以线性方式使用树映射。

树映射在内部表示为带大小界限的树，这是一类支持高效顺序统计查询的自平衡二叉搜索树。

构造子

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

字段

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

内部树映射实现细节。

结构体

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

树映射的良构性谓词。TreeMap 用户无需直接使用它。TreeMap.Raw 用户需要为各引理提供 WF 证明，并应使用 WF.empty、WF.insert 等引理（它们的名称总是与相应操作完全相同）来证明映射操作保持良构性。此类型的构造子属于内部实现细节，用户不应访问。

构造子

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

字段

out : t.inner.WF

内部树映射实现细节。

20.19.9. 依值树映射🔗

本节中的声明应通过 import Std.DTreeMap 导入。

结构体

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)

依值树映射。

树映射存储键到值的分配。它依赖于比较器函数，该函数定义键的排序并提供有效的依赖于顺序的查询，例如检索最小值或最大值。

为了确保操作按预期运行，比较器函数 cmp 应满足一些保证顺序一致的定律：

如果 a 小于（或等于）b，那么 b 大于（或等于）a，反之亦然（参见 OrientedCmp 类型类）。
如果 a 小于或等于 b，且 b 小于或等于 c，那么 a 小于或等于 c（参见 TransCmp 类型类）。

cmp a b = Ordering.eq 的键被认为是相同的，即树映射中只能有一个键为 a 或 b 的条目。查找 a 或 b 始终会产生相同的条目（如果存在）。 dependent 树映射的 get 操作还需要一个 LawfulEqCmp 实例，以确保 cmp a b = .eq 始终隐含 a = b，以便它们各自的值类型相等。

为了避免昂贵的复制，用户应确保线性使用树映射。

在内部，树映射表示为大小有界树，这是一种具有高效顺序统计查找的自平衡二叉搜索树。

为了在证明中使用，应该首选扩展依值树映射的类型 Std.ExtDTreeMap。该类型带有多个外延引理并提供相同的功能，但需要 TransCmp 实例才能使用。

这些树映射包含内置的良构不变量，这意味着它们不能在嵌套归纳类型中使用。对于这些用例，Std.DTreeMap.Raw 和 Std.DTreeMap.Raw.WF 将不变量与树映射分离。如有疑问，请优先选择 DTreeMap 而不是 DTreeMap.Raw。

20.19.9.1. 创建🔗

定义

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

创建一个新的空树映射。还可以并建议使用空集合符号 ∅ 和 {} 来创建空树映射。 simp 将 empty 替换为 ∅。

20.19.9.2. 性质🔗

定义

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

返回映射中存在的映射数量。

定义

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

如果树映射不包含映射，则返回 true。

20.19.9.3. 查询🔗

定义

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

返回值为 true 的条件是：存在给定键 a 的映射，或存在等于 a（按比较器 cmp 判断）的键。还有一个 Prop 值的版本：a ∈ t 相当于 t.contains a = true。

请注意，这与列表的行为不同：对于列表，∈ 使用 = 和 contains 使用 == 进行相等性检查，而对于树映射，两者都使用给定的比较器 cmp。

定义

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

给出给定键的映射存在的证明，检索给定键的映射。

使用 LawfulEqCmp 实例将检索到的值转换为正确的类型。

定义

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

尝试检索给定键的映射，如果不存在此类映射，则会触发 panic。

使用 LawfulEqCmp 实例将检索到的值转换为正确的类型。

定义

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)

尝试检索给定键的映射，如果不存在此类映射，则返回 none。

使用 LawfulEqCmp 实例将检索到的值转换为正确的类型。

定义

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

尝试检索给定键的映射，如果不存在此类映射，则返回 fallback。

使用 LawfulEqCmp 实例将检索到的值转换为正确的类型。

定义

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) : α

从映射中检索与 a 匹配的键。通过要求 a ∈ m 的证明来确保此类映射的存在。结果保证是等于映射中的键的指针。

定义

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 : α) : α

检查给定键的映射是否存在，如果存在则返回该键，否则会触发 panic。如果未触发 panic，结果保证是等于映射中的键的指针。

定义

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 α

检查给定键的映射是否存在，如果存在则返回该键，否则返回 none。 some 情况下的结果保证是等于映射中的键的指针。

定义

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 : α) : α

检查给定键的映射是否存在，如果存在则返回该键，否则返回 fallback。如果存在映射，则保证结果是等于映射中键的指针。

定义

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 α

按升序返回树映射中存在的所有键的列表。

定义

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 α

返回树映射中按升序排列的所有键的数组。

定义

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 β

按升序返回树映射中存在的所有值的列表。

定义

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 β

返回树映射中按升序排列的所有值的数组。

20.19.9.4. 修改🔗

定义

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

就地修改与给定键关联的值，允许通过 Option 值替换函数创建新值和删除值。

此函数可确保线性使用该值。

定义

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

就地修改与给定键关联的值。

此函数可确保线性使用该值。

定义

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

检查映射中是否存在某个键并无条件插入该键的值。

相当于（但可能比）调用 contains 后跟 insert 更快。

定义

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

检查映射中是否存在某个键，如果未找到，则为该键插入一个值。如果返回的 Bool 是 true，则返回的映射不变。如果 Bool 是 false，则返回的映射已插入新值。

相当于（但可能比）调用 contains 后跟 insertIfNew 更快。

定义

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

删除给定键的映射（如果存在）。

定义

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

删除给定函数返回 false 的映射的所有映射。

定义

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

通过将给定函数应用于所有映射来更新映射的值，仅保留函数返回 some 值的映射。

定义

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

将给定的映射插入到映射中。如果给定键已经存在映射，则键和值都将被替换。

定义

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

如果给定键没有映射，则将给定映射插入到映射中。否则，返回未更改的映射。

定义

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

检查映射中是否存在某个键，返回关联的值，如果未找到，则为该键插入一个值。

如果返回值为 some v，则返回的映射不变。如果是 none，则返回的映射已插入新值。

相当于（但可能比）调用 get? 后跟 insertIfNew 更快。

使用 LawfulEqCmp 实例将检索到的值转换为正确的类型。

定义

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

通过迭代给定集合并调用 insert 将多个映射插入到树映射中。如果同一键出现多次，则最后一次出现的键优先。

注意：此优先行为适用于 TreeMap、DTreeMap、TreeMap.Raw 和 DTreeMap.Raw。 insertMany 函数在 TreeSet 和 TreeSet.Raw 上的行为不同：它会更喜欢第一次出现。

定义

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

根据谓词将树映射划分为两个树映射。

20.19.9.5. 迭代🔗

定义

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)

返回对依值树映射的条目的有限迭代器。迭代器按顺序生成映射的元素，然后终止。

终止性质：

Finite 实例：始终存在
Productive 实例：始终存在

定义

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 α

返回依值树映射的键上的有限迭代器。迭代器按顺序生成键，然后终止。

键和值类型必须位于同一个宇宙中。

终止性质：

Finite 实例：始终存在
Productive 实例：始终存在

定义

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 β

返回树映射值的有限迭代器。迭代器按顺序产生值，然后终止。

键和值类型必须位于同一个宇宙中。

终止性质：

Finite 实例：始终存在
Productive 实例：始终存在

定义

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

通过将给定函数应用于所有映射来更新映射的值。

定义

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) : δ

按升序将给定函数折叠到映射中的映射上。

定义

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 δ

按升序将给定的单子函数折叠到映射中的映射上。

定义

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 δ

支持 for 循环在 do 块中的构造形式。迭代按升序进行。

定义

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

按升序对树映射中的每个映射执行单子操作。

20.19.9.6. 转换🔗

定义

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

将映射列表转换为树映射。

定义

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)

将树映射转换为按升序排列的映射列表。

定义

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)

将树映射转换为按升序排列的映射列表。

20.19.9.7. 分离式变体🔗

分离式映射会将良构性证明与数据本身分开。这主要在定义嵌套归纳类型时有用。要使用这些变体，请导入模块 Std.DTreeMap.Raw。

结构体

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)

没有内置的良构不变量的依值树映射，适合在嵌套归纳类型中使用。良构的不变量称为 Raw.WF。如有疑问，请优先选择 DTreeMap 而不是 DTreeMap.Raw。关于 Std.DTreeMap.Raw 操作的引理可在模块 Std.Data.DTreeMap.Raw.Lemmas 中找到。

树映射存储键到值的分配。它依赖于比较器函数，该函数定义键的排序并提供有效的依赖于顺序的查询，例如检索最小值或最大值。

为了确保操作按预期运行，比较器函数 cmp 应满足一些保证顺序一致的定律：

如果 a 小于（或等于）b，那么 b 大于（或等于）a，反之亦然（参见 OrientedCmp 类型类）。
如果 a 小于或等于 b，且 b 小于或等于 c，那么 a 小于或等于 c（参见 TransCmp 类型类）。

为了避免昂贵的复制，用户应确保线性使用树映射。

在内部，树映射表示为大小有界树，这是一种具有高效顺序统计查找的自平衡二叉搜索树。

构造子

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

字段

inner : Std.DTreeMap.Internal.Impl α β

树映射的内部实现细节。

结构体

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

树映射的良构谓词。 DTreeMap 的用户不需要与之交互。 DTreeMap.Raw 的用户需要向引理提供 WF 的证明，并且应该使用像 WF.empty 和 WF.insert 这样的引理（它们的命名总是与它们所涉及的操作完全相同）来表明映射操作保持良构。该类型的构造函数是内部实现细节，用户不应访问。

构造子

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

字段

out : t.inner.WF

树映射的内部实现细节。

20.19.10. 基于树的集合🔗

结构体

Std.TreeSet.{u} (α : Type u)
  (cmp : α → α → Ordering := by exact compare) : Type u
Std.TreeSet.{u} (α : Type u)
  (cmp : α → α → Ordering := by
    exact compare) :
  Type u

树集。

树集按特定顺序存储特定类型的元素。它依赖于比较器函数，该函数定义键的排序并提供有效的依赖于顺序的查询，例如检索最小值或最大值。

为了确保操作按预期运行，比较器函数 cmp 应满足某些规则，以确保顺序一致：

如果 a 小于（或等于）b，则 b 大于（或等于）a 反之亦然（请参阅 OrientedCmp 类型类）。
如果 a 小于或等于 b 并且 b 又小于或等于 c，则 a 小于或等于 c（请参阅 TransCmp 类型类）。

cmp a b = Ordering.eq 的键被认为是相同的，即同一时间只能包含其中一个。

为了避免昂贵的副本，用户应确保线性使用树集。

在内部，树集表示为大小有界树，这是一种具有高效顺序统计查找的自平衡二叉搜索树。

为了在证明中使用，应优先选择扩展树集的类型 Std.ExtTreeSet。该类型带有多个外延引理并提供相同的功能，但需要 TransCmp 实例才能使用。

这些树集包含捆绑的格式良好不变量，这意味着它们不能在嵌套归纳类型中使用。对于这些用例，Std.TreeSet.Raw 和 Std.TreeSet.Raw.WF 将不变量从树集中分离出来。如有疑问，请选择 TreeSet 而不是 TreeSet.Raw。

20.19.10.1. 创建🔗

定义

Std.TreeSet.empty.{u} {α : Type u} {cmp : α → α → Ordering} :
  Std.TreeSet α cmp
Std.TreeSet.empty.{u} {α : Type u}
  {cmp : α → α → Ordering} :
  Std.TreeSet α cmp

创建一个新的空树集。还可以并建议使用空集合符号 ∅ 和 {} 来创建空树集。 simp 将 empty 替换为 ∅。

20.19.10.2. 性质🔗

定义

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

如果树集不包含映射，则返回 true。

定义

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

返回映射中条目的数量。

20.19.10.3. 查询🔗

定义

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

返回值为 true 的条件是：集合中包含 a，或包含等于 a（按比较器 cmp 判断）的元素。还有一个 Prop 值的版本：a ∈ t 相当于 t.contains a = true。

请注意，这与列表的行为不同：对于列表，∈ 使用 =，contains 使用 == 进行相等性检查，而对于树集，两者都使用给定的比较器 cmp。

定义

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) : α

从匹配 a 的集合中检索键。通过要求 a ∈ m 的证明来确保此类键存在。结果保证是等于集合中的键的指针。

定义

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 : α) : α

检查是否包含给定的键，如果包含则返回该键，否则会触发 panic。如果未触发 panic，则结果保证是等于集合中的键的指针。

定义

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 α

检查是否包含给定的键，如果包含则返回该键，否则返回 none。 some 情况下的结果保证是与映射中的键相等的指针。

定义

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 : α) : α

检查是否包含给定的键，如果包含则返回该键，否则返回 fallback。如果包含它们的键，则保证结果是等于集合中的键的指针。

20.19.10.3.1. 基于顺序的查询🔗

定义

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) : α

返回 n 第一个最小元素。

定义

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) : α

返回 n 第一个最小元素，或者如果 n 至少为 t.size，则触发 panic。

定义

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 α

返回 n 第一个最小元素，否则返回 none，如果 n 至少为 t.size。

定义

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 : α) : α

返回 n 第一个最小元素，否则返回 fallback，如果 n 至少为 t.size。

定义

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) :
  α

给出此类元素存在的证明，检索大于或等于给定元素的最小元素。

定义

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 : α) : α

尝试检索大于或等于给定元素的最小元素，如果不存在这样的元素，则会触发 panic。

定义

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 α

尝试检索大于或等于给定元素的最小元素，如果不存在此类元素，则返回 none。

定义

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 : α) : α

尝试检索大于或等于给定元素的最小元素，如果不存在此类元素，则返回 fallback。

定义

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) :
  α

给出这样一个元素存在的证明，检索大于给定元素的最小元素。

定义

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 : α) : α

尝试检索大于给定元素的最小元素，如果不存在这样的元素，则会触发 panic。

定义

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 α

尝试检索大于给定元素的最小元素，如果不存在此类元素，则返回 none。

定义

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 : α) : α

尝试检索大于给定元素的最小元素，如果不存在此类元素，则返回 fallback。

定义

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) :
  α

给出此类元素存在的证明，检索小于或等于给定元素的最大元素。

定义

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 : α) : α

尝试检索小于或等于给定元素的最大元素，如果不存在这样的元素，则会触发 panic。

定义

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 α

尝试检索小于或等于给定元素的最大元素，如果不存在此类元素，则返回 none。

定义

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 : α) : α

尝试检索小于或等于给定元素的最大元素，如果不存在此类元素，则返回 fallback。

定义

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) :
  α

给出这样一个元素存在的证明，检索小于给定元素的最小元素。

定义

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 : α) : α

尝试检索小于给定元素的最小元素，如果不存在这样的元素，则会触发 panic。

定义

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 α

尝试检索小于给定元素的最小元素，如果不存在此类元素，则返回 none。

定义

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 : α) : α

尝试检索小于给定元素的最小元素，如果不存在此类元素，则返回 fallback。

定义

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) : α

给出树集不为空的证明，检索最小元素。

定义

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) : α

尝试检索树集中的最小元素，如果该集为空，则会触发 panic。

定义

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 α

尝试检索树集合的最小元素，如果集合为空，则返回 none。

定义

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 : α) :
  α

尝试检索树集的最小元素，如果树集为空，则返回 fallback。

定义

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) : α

给出树集不为空的证明，检索最大元素。

定义

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) : α

尝试检索树集中的最大元素，如果该集为空，则会触发 panic。

定义

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 α

尝试检索树集中的最大元素，如果集为空，则返回 none。

定义

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 : α) :
  α

尝试检索树集的最大元素，如果树集为空，则返回 fallback。

20.19.10.4. 修改🔗

定义

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

将给定元素插入集合中。如果树集已经包含与给定元素相等（关于 cmp）的元素，则树集原封不动地返回。

注意：此非替换行为适用于 TreeSet 和 TreeSet.Raw。 insert 函数在 TreeMap、DTreeMap、TreeMap.Raw 和 DTreeMap.Raw 上的行为不同：它将改写现有映射。

定义

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

通过迭代给定集合并调用 insert 将多个元素插入树集中。如果同一元素（相对于 cmp）出现多次，则第一次出现的元素优先。

注意：此优先行为适用于 TreeSet 和 TreeSet.Raw。 insertMany 函数在 TreeMap、DTreeMap、TreeMap.Raw 和 DTreeMap.Raw 上的行为有所不同：它会优先采用最后一次出现。

定义

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

检查集合中是否存在某个元素，如果未找到则插入该元素。如果树集已经包含与给定元素相等的元素（就 cmp 而言），则树集原封不动地返回。

相当于（但可能比）调用 contains，然后调用 insert。

定义

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

删除给定的键（如果存在）。

定义

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

通过迭代给定的集合并调用擦除来从树集中删除多个项目。

定义

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

从树集中删除给定函数返回 false 的所有元素。

定义

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

返回包含 t₁ 和 `t2 的所有映射的集合。

该函数保证线性使用 t₁。因此，只要 t₁ 未被共享，其性能特征就可用以下命令式过程描述：遍历 t₂ 中的所有映射并将其插入 t₁。

因此，只要 t₁ 未共享，此方法的运行时间就以 t₂ 的大小呈线性缩放，并以 t₁ 的大小呈对数缩放。

定义

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

根据谓词将树集划分为两个树集。

20.19.10.5. 迭代🔗

定义

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 α

返回树集条目上的有限迭代器。迭代器按顺序产生集合的元素，然后终止。

终止属性：

Finite 实例：始终
Productive 实例：始终

定义

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

检查是否有任何元素满足谓词，如果谓词成功则短路。

定义

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

检查是否所有元素都满足谓词，如果谓词失败则短路。

定义

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) : δ

按升序将给定函数折叠到树集中的元素上。

定义

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 δ

通过按升序将给定函数折叠到树集中的元素上，单子地计算一个值。

定义

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) : δ

按降序将给定函数折叠到树集中的元素上。

定义

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 δ

通过按降序将给定函数折叠到树集中的元素上，单子地计算一个值。

定义

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 δ

支持 for 循环在 do 块中的构造形式。迭代按升序进行。

定义

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

按升序对树集中的每个元素执行单子操作。

20.19.10.6. 转换🔗

定义

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 α

将树集转换为按升序排列的元素列表。

定义

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

将列表转换为树集。

定义

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 α

将树集转换为按升序排列的元素数组。

定义

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

将数组转换为树集。

20.19.10.6.1. 分离式变体🔗

分离式集合会将良构性证明与数据本身分开。这主要在定义嵌套归纳类型时有用。要使用这些变体，请导入模块 Std.TreeSet.Raw。

结构体

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

没有捆绑的格式良好不变量的树集，适合在嵌套归纳类型中使用。格式良好的不变量称为 Raw.WF。如有疑问，请选择 TreeSet 而不是 TreeSet.Raw。关于 Std.TreeSet.Raw 操作的引理可在模块 Std.Data.TreeSet.Raw.Lemmas 中找到。

树集按特定顺序存储特定类型的元素。它依赖于比较器函数，该函数定义键的排序并提供有效的依赖于顺序的查询，例如检索最小值或最大值。

为了确保操作按预期运行，比较器函数 cmp 应满足某些规则，以确保顺序一致：

如果 a 小于（或等于）b，则 b 大于（或等于）a 反之亦然（请参阅 OrientedCmp 类型类）。
如果 a 小于或等于 b 并且 b 又小于或等于 c，则 a 小于或等于 c（请参阅 TransCmp 类型类）。

cmp a b = Ordering.eq 的键被认为是相同的，即只有其中一个可以同时包含在单个树集中。

为了避免昂贵的副本，用户应确保线性使用树集。

在内部，树集表示为大小有界树，这是一种具有高效顺序统计查找的自平衡二叉搜索树。

构造子

Std.TreeSet.Raw.mk.{u}

字段

inner : Std.TreeMap.Raw α Unit cmp

树集合的内部实现细节。

结构体

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

树集的格式良好谓词。 TreeSet 的用户不需要与之交互。 TreeSet.Raw 的用户需要向引理提供 WF 的证明，并且应该使用像 WF.empty 和 WF.insert 这样的引理（它们的命名总是与它们所涉及的操作完全相同）来表明集合操作保持格式良好。该类型的构造函数是内部实现细节，用户不应访问。

构造子

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

字段

out : t.inner.WF

树映射的内部实现细节。

20.1.	自然数
20.2.	整数
20.3.	有限自然数
20.4.	定精度整数
20.5.	位向量
20.6.	浮点数
20.7.	字符
20.8.	字符串
20.9.	单元类型
20.10.	空类型
20.11.	布尔值
20.12.	可选值
20.13.	元组
20.14.	和类型
20.15.	链表
20.16.	数组
20.17.	字节数组
20.18.	范围
20.19.	映射与集合
20.20.	子类型
20.21.	惰性计算