Documentation

Std.Data.DHashMap.Internal.AssocList.Lemmas

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: Connecting operations on AssocList to operations defined in List.Associative

@[simp]
theorem Std.DHashMap.Internal.AssocList.toList_nil {α : Type u} {β : αType v} :
Std.DHashMap.Internal.AssocList.nil.toList = []
@[simp]
theorem Std.DHashMap.Internal.AssocList.toList_cons {α : Type u} {β : αType v} {l : Std.DHashMap.Internal.AssocList α β} {a : α} {b : β a} :
(Std.DHashMap.Internal.AssocList.cons a b l).toList = a, b :: l.toList
@[simp]
theorem Std.DHashMap.Internal.AssocList.foldl_eq {α : Type u} {β : αType v} {δ : Type w} {f : δ(a : α) → β aδ} {init : δ} {l : Std.DHashMap.Internal.AssocList α β} :
Std.DHashMap.Internal.AssocList.foldl f init l = List.foldl (fun (d : δ) (p : (a : α) × β a) => f d p.fst p.snd) init l.toList
@[simp]
theorem Std.DHashMap.Internal.AssocList.length_eq {α : Type u} {β : αType v} {l : Std.DHashMap.Internal.AssocList α β} :
l.length = l.toList.length
@[simp]
theorem Std.DHashMap.Internal.AssocList.getCastD_eq {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : Std.DHashMap.Internal.AssocList α β} {a : α} {fallback : β a} :
@[simp]
theorem Std.DHashMap.Internal.AssocList.getD_eq {α : Type u} {β : Type v} [BEq α] {l : Std.DHashMap.Internal.AssocList α fun (x : α) => β} {a : α} {fallback : β} :
@[simp]
theorem Std.DHashMap.Internal.AssocList.panicWithPosWithDecl_eq {α : Type u} [Inhabited α] {modName : String} {declName : String} {line : Nat} {col : Nat} {msg : String} :
panicWithPosWithDecl modName declName line col msg = default
@[simp]
theorem Std.DHashMap.Internal.AssocList.getKeyD_eq {α : Type u} {β : αType v} [BEq α] {l : Std.DHashMap.Internal.AssocList α β} {a : α} {fallback : α} :
theorem Std.DHashMap.Internal.AssocList.toList_filterMap {α : Type u} {β : αType v} {γ : αType w} {f : (a : α) → β aOption (γ a)} {l : Std.DHashMap.Internal.AssocList α β} :
(Std.DHashMap.Internal.AssocList.filterMap f l).toList.Perm (List.filterMap (fun (p : (a : α) × β a) => Option.map (fun (x : γ p.fst) => p.fst, x) (f p.fst p.snd)) l.toList)
theorem Std.DHashMap.Internal.AssocList.toList_map {α : Type u} {β : αType v} {γ : αType w} {f : (a : α) → β aγ a} {l : Std.DHashMap.Internal.AssocList α β} :
(Std.DHashMap.Internal.AssocList.map f l).toList.Perm (List.map (fun (p : (a : α) × β a) => p.fst, f p.fst p.snd) l.toList)
theorem Std.DHashMap.Internal.AssocList.toList_filter {α : Type u} {β : αType v} {f : (a : α) → β aBool} {l : Std.DHashMap.Internal.AssocList α β} :
(Std.DHashMap.Internal.AssocList.filter f l).toList.Perm (List.filter (fun (p : (a : α) × β a) => f p.fst p.snd) l.toList)