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: tiny private implementation of List.Perm

inductive Std.DHashMap.Internal.List.Perm {α : Type u} : List α → List α → Prop

Internal implementation detail of the hash map

• refl: ∀ {α : Type u} (l : List α), Std.DHashMap.Internal.List.Perm l l

  Internal implementation detail of the hash map

• cons: ∀ {α : Type u} {l l' : List α} (a : α), Std.DHashMap.Internal.List.Perm l l' → Std.DHashMap.Internal.List.Perm (a :: l) (a :: l')

  Internal implementation detail of the hash map

• swap: ∀ {α : Type u} {l l' : List α} (a b : α), Std.DHashMap.Internal.List.Perm l l' → Std.DHashMap.Internal.List.Perm (a :: b :: l) (b :: a :: l)

  Internal implementation detail of the hash map

• trans: ∀ {α : Type u} {l l' l'' : List α}, Std.DHashMap.Internal.List.Perm l l' → Std.DHashMap.Internal.List.Perm l' l'' → Std.DHashMap.Internal.List.Perm l l''

  Internal implementation detail of the hash map

theorem Std.DHashMap.Internal.List.Perm.append_right {α : Type u} {l₁ : List α} {l₂ : List α} (l₃ : List α) (h : Std.DHashMap.Internal.List.Perm l₁ l₂) : Std.DHashMap.Internal.List.Perm (l₁ ++ l₃) (l₂ ++ l₃)

theorem Std.DHashMap.Internal.List.Perm.symm {α : Type u} {l₁ : List α} {l₂ : List α} (h : Std.DHashMap.Internal.List.Perm l₁ l₂) : Std.DHashMap.Internal.List.Perm l₂ l₁

theorem Std.DHashMap.Internal.List.perm_middle {α : Type u} {l₁ : List α} {l₂ : List α} {a : α} : Std.DHashMap.Internal.List.Perm (l₁ ++ a :: l₂) (a :: (l₁ ++ l₂))

theorem Std.DHashMap.Internal.List.perm_append_comm {α : Type u} {l₁ : List α} {l₂ : List α} : Std.DHashMap.Internal.List.Perm (l₁ ++ l₂) (l₂ ++ l₁)

theorem Std.DHashMap.Internal.List.Perm.append_left {α : Type u} (l₁ : List α) {l₂ : List α} {l₃ : List α} (h : Std.DHashMap.Internal.List.Perm l₂ l₃) : Std.DHashMap.Internal.List.Perm (l₁ ++ l₂) (l₁ ++ l₃)

theorem Std.DHashMap.Internal.List.Perm.append {α : Type u} {l₁ : List α} {l₂ : List α} {l₃ : List α} {l₄ : List α} (h₁ : Std.DHashMap.Internal.List.Perm l₁ l₂) (h₂ : Std.DHashMap.Internal.List.Perm l₃ l₄) : Std.DHashMap.Internal.List.Perm (l₁ ++ l₃) (l₂ ++ l₄)

theorem Std.DHashMap.Internal.List.Perm.length_eq {α : Type u} {l : List α} {l' : List α} (h : Std.DHashMap.Internal.List.Perm l l') : l.length = l'.length

@[simp]

theorem Std.DHashMap.Internal.List.not_perm_empty_cons {α : Type u} {l : List α} {a : α} : ¬Std.DHashMap.Internal.List.Perm [] (a :: l)

@[simp]

theorem Std.DHashMap.Internal.List.not_perm_cons_empty {α : Type u} {l : List α} {a : α} : ¬Std.DHashMap.Internal.List.Perm (a :: l) []

theorem Std.DHashMap.Internal.List.Perm.isEmpty_eq {α : Type u} {l : List α} {l' : List α} (h : Std.DHashMap.Internal.List.Perm l l') : l.isEmpty = l'.isEmpty

theorem Std.DHashMap.Internal.List.perm_append_comm_assoc {α : Type u} (l₁ : List α) (l₂ : List α) (l₃ : List α) : Std.DHashMap.Internal.List.Perm (l₁ ++ (l₂ ++ l₃)) (l₂ ++ (l₁ ++ l₃))

theorem Std.DHashMap.Internal.List.Perm.mem_iff {α : Type u} {l₁ : List α} {l₂ : List α} (h : Std.DHashMap.Internal.List.Perm l₁ l₂) {a : α} : a ∈ l₁ ↔ a ∈ l₂

theorem Std.DHashMap.Internal.List.Perm.map {α : Type u} {β : Type v} (f : α → β) {l₁ : List α} {l₂ : List α} (h : Std.DHashMap.Internal.List.Perm l₁ l₂) : Std.DHashMap.Internal.List.Perm (List.map f l₁) (List.map f l₂)

theorem Std.DHashMap.Internal.List.reverse_perm {α : Type u} {l : List α} : Std.DHashMap.Internal.List.Perm l.reverse l