This is an internal implementation file of the hash map. Users of the hash map should not rely on the contents of this file.

File contents: definitions on lists needed to state the well-formedness predicate

def Std.DHashMap.Internal.List.Pairwise {α : Type u} (P : α → α → Prop) : List α → Prop

Internal implementation detail of the hash map

Equations

• Std.DHashMap.Internal.List.Pairwise P [] = True
• Std.DHashMap.Internal.List.Pairwise P (x_1 :: xs) = ((∀ (y : α), y ∈ xs → P x_1 y) ∧ Std.DHashMap.Internal.List.Pairwise P xs)

def Std.DHashMap.Internal.List.keys {α : Type u} {β : α → Type v} : List ((a : α) × β a) → List α

Internal implementation detail of the hash map

Equations

• Std.DHashMap.Internal.List.keys [] = []
• Std.DHashMap.Internal.List.keys (⟨k, snd⟩ :: l) = k :: Std.DHashMap.Internal.List.keys l

structure Std.DHashMap.Internal.List.DistinctKeys {α : Type u} {β : α → Type v} [BEq α] (l : List ((a : α) × β a)) : Prop

Internal implementation detail of the hash map

• distinct : Std.DHashMap.Internal.List.Pairwise (fun (a b : α) => (a == b) = false) (Std.DHashMap.Internal.List.keys l)

  Internal implementation detail of the hash map

theorem Std.DHashMap.Internal.List.DistinctKeys.distinct {α : Type u} {β : α → Type v} [BEq α] {l : List ((a : α) × β a)} (self : Std.DHashMap.Internal.List.DistinctKeys l) : Std.DHashMap.Internal.List.Pairwise (fun (a b : α) => (a == b) = false) (Std.DHashMap.Internal.List.keys l)

Internal implementation detail of the hash map

def Std.DHashMap.Internal.List.values {α : Type u} {β : Type v} : List ((_ : α) × β) → List β

Internal implementation detail of the hash map

Equations

• Std.DHashMap.Internal.List.values [] = []
• Std.DHashMap.Internal.List.values (⟨fst, v⟩ :: l) = v :: Std.DHashMap.Internal.List.values l