Documentation

Std.Data.DHashMap.Internal.List.Associative

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: Verification of associative lists

theorem Std.DHashMap.Internal.List.assoc_induction {α : Type u} {β : αType v} {motive : List ((a : α) × β a)Prop} (nil : motive []) (cons : ∀ (k : α) (v : β k) (tail : List ((a : α) × β a)), motive tailmotive (k, v :: tail)) (t : List ((a : α) × β a)) :
motive t
def Std.DHashMap.Internal.List.getEntry? {α : Type u} {β : αType v} [BEq α] (a : α) :
List ((a : α) × β a)Option ((a : α) × β a)

Internal implementation detail of the hash map

Equations
Instances For
    @[simp]
    theorem Std.DHashMap.Internal.List.getEntry?_nil {α : Type u} {β : αType v} [BEq α] {a : α} :
    theorem Std.DHashMap.Internal.List.getEntry?_cons {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} {a : α} {v : β k} :
    Std.DHashMap.Internal.List.getEntry? a (k, v :: l) = bif k == a then some k, v else Std.DHashMap.Internal.List.getEntry? a l
    theorem Std.DHashMap.Internal.List.getEntry?_cons_of_true {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} {a : α} {v : β k} (h : (k == a) = true) :
    Std.DHashMap.Internal.List.getEntry? a (k, v :: l) = some k, v
    theorem Std.DHashMap.Internal.List.getEntry?_cons_of_false {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} {a : α} {v : β k} (h : (k == a) = false) :
    @[simp]
    theorem Std.DHashMap.Internal.List.getEntry?_cons_self {α : Type u} {β : αType v} [BEq α] [ReflBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
    Std.DHashMap.Internal.List.getEntry? k (k, v :: l) = some k, v
    theorem Std.DHashMap.Internal.List.getEntry?_eq_some {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {a : α} {p : (a : α) × β a} (h : Std.DHashMap.Internal.List.getEntry? a l = some p) :
    (p.fst == a) = true
    theorem Std.DHashMap.Internal.List.getEntry?_congr {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a : α} {b : α} (h : (a == b) = true) :
    theorem Std.DHashMap.Internal.List.isEmpty_eq_false_iff_exists_isSome_getEntry? {α : Type u} {β : αType v} [BEq α] [ReflBEq α] {l : List ((a : α) × β a)} :
    l.isEmpty = false ∃ (a : α), (Std.DHashMap.Internal.List.getEntry? a l).isSome = true
    theorem Std.DHashMap.Internal.List.isEmpty_iff_forall_isSome_getEntry? {α : Type u} {β : αType v} [BEq α] [ReflBEq α] {l : List ((a : α) × β a)} :
    l.isEmpty = true ∀ (a : α), (Std.DHashMap.Internal.List.getEntry? a l).isSome = false
    def Std.DHashMap.Internal.List.getValue? {α : Type u} {β : Type v} [BEq α] (a : α) :
    List ((_ : α) × β)Option β

    Internal implementation detail of the hash map

    Equations
    Instances For
      @[simp]
      theorem Std.DHashMap.Internal.List.getValue?_cons {α : Type u} {β : Type v} [BEq α] {l : List ((_ : α) × β)} {k : α} {a : α} {v : β} :
      theorem Std.DHashMap.Internal.List.getValue?_cons_of_true {α : Type u} {β : Type v} [BEq α] {l : List ((_ : α) × β)} {k : α} {a : α} {v : β} (h : (k == a) = true) :
      theorem Std.DHashMap.Internal.List.getValue?_cons_of_false {α : Type u} {β : Type v} [BEq α] {l : List ((_ : α) × β)} {k : α} {a : α} {v : β} (h : (k == a) = false) :
      @[simp]
      theorem Std.DHashMap.Internal.List.getValue?_cons_self {α : Type u} {β : Type v} [BEq α] [ReflBEq α] {l : List ((_ : α) × β)} {k : α} {v : β} :
      theorem Std.DHashMap.Internal.List.getValue?_eq_getEntry? {α : Type u} {β : Type v} [BEq α] {l : List ((_ : α) × β)} {a : α} :
      theorem Std.DHashMap.Internal.List.getValue?_congr {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {a : α} {b : α} (h : (a == b) = true) :
      theorem Std.DHashMap.Internal.List.isEmpty_eq_false_iff_exists_isSome_getValue? {α : Type u} {β : Type v} [BEq α] [ReflBEq α] {l : List ((_ : α) × β)} :
      l.isEmpty = false ∃ (a : α), (Std.DHashMap.Internal.List.getValue? a l).isSome = true
      def Std.DHashMap.Internal.List.getValueCast? {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] (a : α) :
      List ((a : α) × β a)Option (β a)

      Internal implementation detail of the hash map

      Equations
      Instances For
        @[simp]
        theorem Std.DHashMap.Internal.List.getValueCast?_cons {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {a : α} {v : β k} :
        theorem Std.DHashMap.Internal.List.getValueCast?_cons_of_true {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {a : α} {v : β k} (h : (k == a) = true) :
        theorem Std.DHashMap.Internal.List.getValueCast?_cons_of_false {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {a : α} {v : β k} (h : (k == a) = false) :
        @[simp]
        theorem Std.DHashMap.Internal.List.getValueCast?_cons_self {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
        theorem Std.DHashMap.Internal.List.isEmpty_eq_false_iff_exists_isSome_getValueCast? {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} :
        l.isEmpty = false ∃ (a : α), (Std.DHashMap.Internal.List.getValueCast? a l).isSome = true
        def Std.DHashMap.Internal.List.containsKey {α : Type u} {β : αType v} [BEq α] (a : α) :
        List ((a : α) × β a)Bool

        Internal implementation detail of the hash map

        Equations
        Instances For
          @[simp]
          theorem Std.DHashMap.Internal.List.containsKey_cons {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} {a : α} {v : β k} :
          theorem Std.DHashMap.Internal.List.containsKey_cons_eq_false {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} {a : α} {v : β k} :
          theorem Std.DHashMap.Internal.List.containsKey_cons_eq_true {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} {a : α} {v : β k} :
          theorem Std.DHashMap.Internal.List.containsKey_cons_of_beq {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} {a : α} {v : β k} (h : (k == a) = true) :
          @[simp]
          theorem Std.DHashMap.Internal.List.containsKey_cons_self {α : Type u} {β : αType v} [BEq α] [ReflBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
          theorem Std.DHashMap.Internal.List.containsKey_cons_of_containsKey {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} {a : α} {v : β k} (h : Std.DHashMap.Internal.List.containsKey a l = true) :
          theorem Std.DHashMap.Internal.List.containsKey_of_containsKey_cons {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} {a : α} {v : β k} (h₁ : Std.DHashMap.Internal.List.containsKey a (k, v :: l) = true) (h₂ : (k == a) = false) :
          theorem Std.DHashMap.Internal.List.isEmpty_eq_false_of_containsKey {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {a : α} (h : Std.DHashMap.Internal.List.containsKey a l = true) :
          l.isEmpty = false
          theorem Std.DHashMap.Internal.List.isEmpty_eq_false_iff_exists_containsKey {α : Type u} {β : αType v} [BEq α] [ReflBEq α] {l : List ((a : α) × β a)} :
          theorem Std.DHashMap.Internal.List.isEmpty_iff_forall_containsKey {α : Type u} {β : αType v} [BEq α] [ReflBEq α] {l : List ((a : α) × β a)} :
          @[simp]
          theorem Std.DHashMap.Internal.List.getEntry?_eq_none {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {a : α} :
          theorem Std.DHashMap.Internal.List.containsKey_congr {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a : α} {b : α} (h : (a == b) = true) :
          theorem Std.DHashMap.Internal.List.containsKey_of_beq {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a : α} {b : α} (hla : Std.DHashMap.Internal.List.containsKey a l = true) (hab : (a == b) = true) :
          def Std.DHashMap.Internal.List.getEntry {α : Type u} {β : αType v} [BEq α] (a : α) (l : List ((a : α) × β a)) (h : Std.DHashMap.Internal.List.containsKey a l = true) :
          (a : α) × β a

          Internal implementation detail of the hash map

          Equations
          Instances For
            theorem Std.DHashMap.Internal.List.getEntry_eq_of_getEntry?_eq_some {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} {a : α} {v : β k} (h : Std.DHashMap.Internal.List.getEntry? a l = some k, v) {h' : Std.DHashMap.Internal.List.containsKey a l = true} :
            theorem Std.DHashMap.Internal.List.getEntry_cons_of_beq {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} {a : α} {v : β k} (h : (k == a) = true) :
            Std.DHashMap.Internal.List.getEntry a (k, v :: l) = k, v
            @[simp]
            theorem Std.DHashMap.Internal.List.getEntry_cons_self {α : Type u} {β : αType v} [BEq α] [ReflBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
            Std.DHashMap.Internal.List.getEntry k (k, v :: l) = k, v
            theorem Std.DHashMap.Internal.List.getEntry_cons_of_false {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} {a : α} {v : β k} {h₁ : Std.DHashMap.Internal.List.containsKey a (k, v :: l) = true} (h₂ : (k == a) = false) :
            def Std.DHashMap.Internal.List.getValue {α : Type u} {β : Type v} [BEq α] (a : α) (l : List ((_ : α) × β)) (h : Std.DHashMap.Internal.List.containsKey a l = true) :
            β

            Internal implementation detail of the hash map

            Equations
            Instances For
              theorem Std.DHashMap.Internal.List.getValue_cons_of_beq {α : Type u} {β : Type v} [BEq α] {l : List ((_ : α) × β)} {k : α} {a : α} {v : β} (h : (k == a) = true) :
              @[simp]
              theorem Std.DHashMap.Internal.List.getValue_cons_self {α : Type u} {β : Type v} [BEq α] [ReflBEq α] {l : List ((_ : α) × β)} {k : α} {v : β} :
              theorem Std.DHashMap.Internal.List.getValue_cons_of_false {α : Type u} {β : Type v} [BEq α] {l : List ((_ : α) × β)} {k : α} {a : α} {v : β} {h₁ : Std.DHashMap.Internal.List.containsKey a (k, v :: l) = true} (h₂ : (k == a) = false) :
              theorem Std.DHashMap.Internal.List.getValue_cons {α : Type u} {β : Type v} [BEq α] {l : List ((_ : α) × β)} {k : α} {a : α} {v : β} {h : Std.DHashMap.Internal.List.containsKey a (k, v :: l) = true} :
              Std.DHashMap.Internal.List.getValue a (k, v :: l) h = if h' : (k == a) = true then v else Std.DHashMap.Internal.List.getValue a l
              def Std.DHashMap.Internal.List.getValueCast {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] (a : α) (l : List ((a : α) × β a)) (h : Std.DHashMap.Internal.List.containsKey a l = true) :
              β a

              Internal implementation detail of the hash map

              Equations
              Instances For
                theorem Std.DHashMap.Internal.List.Option.get_congr {α : Type u} {o : Option α} {o' : Option α} {ho : o.isSome = true} (h : o = o') :
                o.get ho = o'.get
                theorem Std.DHashMap.Internal.List.getValueCast_cons {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {a : α} {v : β k} (h : Std.DHashMap.Internal.List.containsKey a (k, v :: l) = true) :
                Std.DHashMap.Internal.List.getValueCast a (k, v :: l) h = if h' : (k == a) = true then cast v else Std.DHashMap.Internal.List.getValueCast a l
                def Std.DHashMap.Internal.List.getValueCastD {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] (a : α) (l : List ((a : α) × β a)) (fallback : β a) :
                β a

                Internal implementation detail of the hash map

                Equations
                Instances For
                  @[simp]
                  theorem Std.DHashMap.Internal.List.getValueCastD_nil {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {a : α} {fallback : β a} :
                  theorem Std.DHashMap.Internal.List.getValueCastD_eq_getValueCast? {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} {fallback : β a} :
                  theorem Std.DHashMap.Internal.List.getValueCastD_eq_fallback {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} {fallback : β a} (h : Std.DHashMap.Internal.List.containsKey a l = false) :
                  def Std.DHashMap.Internal.List.getValueCast! {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] (a : α) [Inhabited (β a)] (l : List ((a : α) × β a)) :
                  β a

                  Internal implementation detail of the hash map

                  Equations
                  Instances For
                    @[simp]
                    theorem Std.DHashMap.Internal.List.getValueCast!_nil {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {a : α} [Inhabited (β a)] :
                    theorem Std.DHashMap.Internal.List.getValueCast!_eq_default {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} [Inhabited (β a)] (h : Std.DHashMap.Internal.List.containsKey a l = false) :
                    def Std.DHashMap.Internal.List.getValueD {α : Type u} {β : Type v} [BEq α] (a : α) (l : List ((_ : α) × β)) (fallback : β) :
                    β

                    Internal implementation detail of the hash map

                    Equations
                    Instances For
                      @[simp]
                      theorem Std.DHashMap.Internal.List.getValueD_nil {α : Type u} {β : Type v} [BEq α] {a : α} {fallback : β} :
                      theorem Std.DHashMap.Internal.List.getValueD_eq_getValue? {α : Type u} {β : Type v} [BEq α] {l : List ((_ : α) × β)} {a : α} {fallback : β} :
                      theorem Std.DHashMap.Internal.List.getValueD_eq_fallback {α : Type u} {β : Type v} [BEq α] {l : List ((_ : α) × β)} {a : α} {fallback : β} (h : Std.DHashMap.Internal.List.containsKey a l = false) :
                      theorem Std.DHashMap.Internal.List.getValueD_eq_getValueCastD {α : Type u} {β : Type v} [BEq α] [LawfulBEq α] {l : List ((_ : α) × β)} {a : α} {fallback : β} :
                      theorem Std.DHashMap.Internal.List.getValueD_congr {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {a : α} {b : α} {fallback : β} (hab : (a == b) = true) :
                      def Std.DHashMap.Internal.List.getValue! {α : Type u} {β : Type v} [BEq α] [Inhabited β] (a : α) (l : List ((_ : α) × β)) :
                      β

                      Internal implementation detail of the hash map

                      Equations
                      Instances For
                        @[simp]
                        theorem Std.DHashMap.Internal.List.getValue!_nil {α : Type u} {β : Type v} [BEq α] [Inhabited β] {a : α} :
                        theorem Std.DHashMap.Internal.List.getValue!_congr {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] [Inhabited β] {l : List ((_ : α) × β)} {a : α} {b : α} (hab : (a == b) = true) :
                        def Std.DHashMap.Internal.List.replaceEntry {α : Type u} {β : αType v} [BEq α] (k : α) (v : β k) :
                        List ((a : α) × β a)List ((a : α) × β a)

                        Internal implementation detail of the hash map

                        Equations
                        Instances For
                          @[simp]
                          theorem Std.DHashMap.Internal.List.replaceEntry_nil {α : Type u} {β : αType v} [BEq α] {k : α} {v : β k} :
                          theorem Std.DHashMap.Internal.List.replaceEntry_cons {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} {k' : α} {v : β k} {v' : β k'} :
                          Std.DHashMap.Internal.List.replaceEntry k v (k', v' :: l) = bif k' == k then k, v :: l else k', v' :: Std.DHashMap.Internal.List.replaceEntry k v l
                          theorem Std.DHashMap.Internal.List.replaceEntry_cons_of_true {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} {k' : α} {v : β k} {v' : β k'} (h : (k' == k) = true) :
                          Std.DHashMap.Internal.List.replaceEntry k v (k', v' :: l) = k, v :: l
                          theorem Std.DHashMap.Internal.List.replaceEntry_cons_of_false {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} {k' : α} {v : β k} {v' : β k'} (h : (k' == k) = false) :
                          @[simp]
                          theorem Std.DHashMap.Internal.List.isEmpty_replaceEntry {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
                          (Std.DHashMap.Internal.List.replaceEntry k v l).isEmpty = l.isEmpty
                          theorem Std.DHashMap.Internal.List.getEntry?_replaceEntry_of_true {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a : α} {k : α} {v : β k} (hl : Std.DHashMap.Internal.List.containsKey k l = true) (h : (k == a) = true) :
                          @[simp]
                          theorem Std.DHashMap.Internal.List.length_replaceEntry {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
                          def Std.DHashMap.Internal.List.eraseKey {α : Type u} {β : αType v} [BEq α] (k : α) :
                          List ((a : α) × β a)List ((a : α) × β a)

                          Internal implementation detail of the hash map

                          Equations
                          Instances For
                            @[simp]
                            theorem Std.DHashMap.Internal.List.eraseKey_nil {α : Type u} {β : αType v} [BEq α] {k : α} :
                            theorem Std.DHashMap.Internal.List.eraseKey_cons {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} {k' : α} {v' : β k'} :
                            Std.DHashMap.Internal.List.eraseKey k (k', v' :: l) = bif k' == k then l else k', v' :: Std.DHashMap.Internal.List.eraseKey k l
                            theorem Std.DHashMap.Internal.List.eraseKey_cons_of_beq {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} {k' : α} {v' : β k'} (h : (k' == k) = true) :
                            @[simp]
                            theorem Std.DHashMap.Internal.List.eraseKey_cons_self {α : Type u} {β : αType v} [BEq α] [ReflBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
                            theorem Std.DHashMap.Internal.List.eraseKey_cons_of_false {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} {k' : α} {v' : β k'} (h : (k' == k) = false) :
                            theorem Std.DHashMap.Internal.List.length_eraseKey {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} :
                            (Std.DHashMap.Internal.List.eraseKey k l).length = if Std.DHashMap.Internal.List.containsKey k l = true then l.length - 1 else l.length
                            theorem Std.DHashMap.Internal.List.length_eraseKey_le {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} :
                            theorem Std.DHashMap.Internal.List.length_le_length_eraseKey {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} :
                            l.length (Std.DHashMap.Internal.List.eraseKey k l).length + 1
                            theorem Std.DHashMap.Internal.List.isEmpty_eraseKey {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} :
                            @[simp]
                            theorem Std.DHashMap.Internal.List.keys_cons {α : Type u} {β : αType v} {l : List ((a : α) × β a)} {k : α} {v : β k} :
                            theorem Std.DHashMap.Internal.List.keys_eq_map {α : Type u} {β : αType v} (l : List ((a : α) × β a)) :
                            Std.DHashMap.Internal.List.keys l = List.map (fun (x : (a : α) × β a) => x.fst) l
                            theorem Std.DHashMap.Internal.List.containsKey_eq_true_iff_exists_mem {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {a : α} :
                            Std.DHashMap.Internal.List.containsKey a l = true ∃ (p : (a : α) × β a), p l (p.fst == a) = true
                            theorem Std.DHashMap.Internal.List.containsKey_of_mem {α : Type u} {β : αType v} [BEq α] [ReflBEq α] {l : List ((a : α) × β a)} {p : (a : α) × β a} (hp : p l) :
                            theorem Std.DHashMap.Internal.List.containsKey_iff_exists {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a : α} :
                            theorem Std.DHashMap.Internal.List.DistinctKeys.tail {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
                            theorem Std.DHashMap.Internal.List.DistinctKeys.containsKey_eq_false {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
                            theorem Std.DHashMap.Internal.List.mem_iff_getEntry?_eq_some {α : Type u} {β : αType v} [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {p : (a : α) × β a} (h : Std.DHashMap.Internal.List.DistinctKeys l) :
                            def Std.DHashMap.Internal.List.insertEntry {α : Type u} {β : αType v} [BEq α] (k : α) (v : β k) (l : List ((a : α) × β a)) :
                            List ((a : α) × β a)

                            Internal implementation detail of the hash map

                            Equations
                            Instances For
                              @[simp]
                              theorem Std.DHashMap.Internal.List.insertEntry_nil {α : Type u} {β : αType v} [BEq α] {k : α} {v : β k} :
                              theorem Std.DHashMap.Internal.List.insertEntry_of_containsKey_eq_false {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} (h : Std.DHashMap.Internal.List.containsKey k l = false) :
                              @[simp]
                              theorem Std.DHashMap.Internal.List.isEmpty_insertEntry {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
                              theorem Std.DHashMap.Internal.List.length_insertEntry {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
                              (Std.DHashMap.Internal.List.insertEntry k v l).length = if Std.DHashMap.Internal.List.containsKey k l = true then l.length else l.length + 1
                              theorem Std.DHashMap.Internal.List.length_le_length_insertEntry {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
                              theorem Std.DHashMap.Internal.List.length_insertEntry_le {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
                              (Std.DHashMap.Internal.List.insertEntry k v l).length l.length + 1
                              theorem Std.DHashMap.Internal.List.getValue?_insertEntry_of_beq {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k : α} {a : α} {v : β} (h : (k == a) = true) :
                              theorem Std.DHashMap.Internal.List.getEntry?_insertEntry {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} {a : α} {v : β k} :
                              theorem Std.DHashMap.Internal.List.getValueCast?_insertEntry {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {a : α} {v : β k} :
                              theorem Std.DHashMap.Internal.List.getValueCast!_insertEntry {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {a : α} [Inhabited (β a)] {v : β k} :
                              theorem Std.DHashMap.Internal.List.getValueCast!_insertEntry_self {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} [Inhabited (β k)] {v : β k} :
                              theorem Std.DHashMap.Internal.List.getValueCastD_insertEntry {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {a : α} {fallback : β a} {v : β k} :
                              theorem Std.DHashMap.Internal.List.getValueCastD_insertEntry_self {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {fallback : β k} {v : β k} :
                              theorem Std.DHashMap.Internal.List.getValueD_insertEntry {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k : α} {a : α} {fallback : β} {v : β} :
                              theorem Std.DHashMap.Internal.List.getValueD_insertEntry_self {α : Type u} {β : Type v} [BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {k : α} {fallback : β} {v : β} :
                              @[simp]
                              theorem Std.DHashMap.Internal.List.containsKey_insertEntry_of_beq {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} {a : α} {v : β k} (h : (k == a) = true) :
                              @[simp]
                              theorem Std.DHashMap.Internal.List.containsKey_insertEntry_self {α : Type u} {β : αType v} [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
                              theorem Std.DHashMap.Internal.List.getValueCast_insertEntry_self {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
                              def Std.DHashMap.Internal.List.insertEntryIfNew {α : Type u} {β : αType v} [BEq α] (k : α) (v : β k) (l : List ((a : α) × β a)) :
                              List ((a : α) × β a)

                              Internal implementation detail of the hash map

                              Equations
                              Instances For
                                theorem Std.DHashMap.Internal.List.insertEntryIfNew_of_containsKey {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} (h : Std.DHashMap.Internal.List.containsKey k l = true) :
                                theorem Std.DHashMap.Internal.List.insertEntryIfNew_of_containsKey_eq_false {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} (h : Std.DHashMap.Internal.List.containsKey k l = false) :
                                @[simp]
                                theorem Std.DHashMap.Internal.List.isEmpty_insertEntryIfNew {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :

                                This is a restatement of containsKey_insertEntryIfNew that is written to exactly match the proof obligation in the statement of getValueCast_insertEntryIfNew.

                                theorem Std.DHashMap.Internal.List.getValueCastD_insertEntryIfNew {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {a : α} {v : β k} {fallback : β a} :
                                theorem Std.DHashMap.Internal.List.getValueD_insertEntryIfNew {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k : α} {a : α} {fallback : β} {v : β} :
                                theorem Std.DHashMap.Internal.List.length_insertEntryIfNew {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
                                theorem Std.DHashMap.Internal.List.length_le_length_insertEntryIfNew {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
                                theorem Std.DHashMap.Internal.List.length_insertEntryIfNew_le {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
                                theorem Std.DHashMap.Internal.List.keys_filterMap {α : Type u} {β : αType v} {γ : αType w} [BEq α] {l : List ((a : α) × β a)} {f : (a : α) → β aOption (γ a)} :
                                Std.DHashMap.Internal.List.keys (List.filterMap (fun (p : (a : α) × β a) => Option.map (fun (x : γ p.fst) => p.fst, x) (f p.fst p.snd)) l) = Std.DHashMap.Internal.List.keys (List.filter (fun (p : (a : α) × β a) => (f p.fst p.snd).isSome) l)
                                @[simp]
                                theorem Std.DHashMap.Internal.List.keys_map {α : Type u} {β : αType v} {γ : αType w} [BEq α] {l : List ((a : α) × β a)} {f : (a : α) → β aγ a} :
                                Std.DHashMap.Internal.List.keys (List.map (fun (p : (a : α) × β a) => p.fst, f p.fst p.snd) l) = Std.DHashMap.Internal.List.keys l
                                theorem Std.DHashMap.Internal.List.DistinctKeys.filterMap {α : Type u} {β : αType v} {γ : αType w} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {f : (a : α) → β aOption (γ a)} :
                                Std.DHashMap.Internal.List.DistinctKeys lStd.DHashMap.Internal.List.DistinctKeys (List.filterMap (fun (p : (a : α) × β a) => Option.map (fun (x : γ p.fst) => p.fst, x) (f p.fst p.snd)) l)
                                theorem Std.DHashMap.Internal.List.DistinctKeys.map {α : Type u} {β : αType v} {γ : αType w} [BEq α] {l : List ((a : α) × β a)} {f : (a : α) → β aγ a} (h : Std.DHashMap.Internal.List.DistinctKeys l) :
                                Std.DHashMap.Internal.List.DistinctKeys (List.map (fun (p : (a : α) × β a) => p.fst, f p.fst p.snd) l)
                                theorem Std.DHashMap.Internal.List.DistinctKeys.filter {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {f : (a : α) → β aBool} (h : Std.DHashMap.Internal.List.DistinctKeys l) :
                                Std.DHashMap.Internal.List.DistinctKeys (List.filter (fun (p : (a : α) × β a) => f p.fst p.snd) l)
                                theorem Std.DHashMap.Internal.List.getValueCastD_eraseKey {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {a : α} {fallback : β a} (hl : Std.DHashMap.Internal.List.DistinctKeys l) :
                                theorem Std.DHashMap.Internal.List.getValueCastD_eraseKey_self {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {fallback : β k} (hl : Std.DHashMap.Internal.List.DistinctKeys l) :
                                theorem Std.DHashMap.Internal.List.getValueD_eraseKey {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k : α} {a : α} {fallback : β} (hl : Std.DHashMap.Internal.List.DistinctKeys l) :
                                theorem Std.DHashMap.Internal.List.containsKey_of_perm {α : Type u} {β : αType v} [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {l' : List ((a : α) × β a)} {k : α} (h : Std.DHashMap.Internal.List.Perm l l') :
                                theorem Std.DHashMap.Internal.List.getValueCastD_of_perm {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {l' : List ((a : α) × β a)} {a : α} {fallback : β a} (hl : Std.DHashMap.Internal.List.DistinctKeys l) (h : Std.DHashMap.Internal.List.Perm l l') :
                                theorem Std.DHashMap.Internal.List.getValueD_of_perm {α : Type u} {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {l' : List ((_ : α) × β)} {a : α} {fallback : β} (hl : Std.DHashMap.Internal.List.DistinctKeys l) (h : Std.DHashMap.Internal.List.Perm l l') :
                                theorem Std.DHashMap.Internal.List.perm_cons_getEntry {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {a : α} (h : Std.DHashMap.Internal.List.containsKey a l = true) :
                                @[simp]
                                theorem Std.DHashMap.Internal.List.getEntry?_append {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {l' : List ((a : α) × β a)} {a : α} :
                                @[simp]
                                theorem Std.DHashMap.Internal.List.containsKey_append {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {l' : List ((a : α) × β a)} {a : α} :
                                theorem Std.DHashMap.Internal.List.containsKey_bind_eq_false {α : Type u} {β : αType v} [BEq α] {γ : Type w} {l : List γ} {f : γList ((a : α) × β a)} {a : α} (h : ∀ (i : Nat) (h : i < l.length), Std.DHashMap.Internal.List.containsKey a (f l[i]) = false) :
                                @[simp]
                                theorem Std.DHashMap.Internal.List.getValue?_append {α : Type u} {β : Type v} [BEq α] {l : List ((_ : α) × β)} {l' : List ((_ : α) × β)} {a : α} :
                                theorem Std.DHashMap.Internal.List.replaceEntry_append_of_containsKey_left {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {l' : List ((a : α) × β a)} {k : α} {v : β k} (h : Std.DHashMap.Internal.List.containsKey k l = true) :
                                theorem Std.DHashMap.Internal.List.replaceEntry_append_of_containsKey_left_eq_false {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {l' : List ((a : α) × β a)} {k : α} {v : β k} (h : Std.DHashMap.Internal.List.containsKey k l = false) :
                                theorem Std.DHashMap.Internal.List.replaceEntry_append_of_containsKey_right_eq_false {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {l' : List ((a : α) × β a)} {k : α} {v : β k} (h : Std.DHashMap.Internal.List.containsKey k l' = false) :
                                theorem Std.DHashMap.Internal.List.insertEntry_append_of_not_contains_right {α : Type u} {β : αType v} [BEq α] {l : List ((a : α) × β a)} {l' : List ((a : α) × β a)} {k : α} {v : β k} (h' : Std.DHashMap.Internal.List.containsKey k l' = false) :