Documentation

Std.Data.DHashMap.Internal.List.Pairwise

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.Pairwise

theorem Std.DHashMap.Internal.List.Pairwise.perm {α : Type u} {P : ααProp} (hP : ∀ {x y : α}, P x yP y x) {l : List α} {l' : List α} (h : Std.DHashMap.Internal.List.Perm l l') :
theorem Std.DHashMap.Internal.List.pairwise_cons {α : Type u} {P : ααProp} {a : α} {l : List α} :