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

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

Internal implementation detail of the hash map

Equations

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

Instances For

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

Internal implementation detail of the hash map

- distinct : List.Pairwise (fun (a b : α) => (a == b) = false) (keys l)

  Internal implementation detail of the hash map

Instances For

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

Internal implementation detail of the hash map

Equations

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

Instances For