Documentation

Batteries.Data.AssocList

inductive Batteries.AssocList (α : Type u) (β : Type v) :
Type (max u v)

AssocList α β is "the same as" List (α × β), but flattening the structure leads to one fewer pointer indirection (in the current code generator). It is mainly intended as a component of HashMap, but it can also be used as a plain key-value map.

Instances For
    instance Batteries.instInhabitedAssocList :
    {a : Type u_1} → {a_1 : Type u_2} → Inhabited (Batteries.AssocList a a_1)
    Equations
    • Batteries.instInhabitedAssocList = { default := Batteries.AssocList.nil }
    def Batteries.AssocList.toList {α : Type u_1} {β : Type u_2} :
    Batteries.AssocList α βList (α × β)

    O(n). Convert an AssocList α β into the equivalent List (α × β). This is used to give specifications for all the AssocList functions in terms of corresponding list functions.

    Equations
    Instances For
      Equations
      • Batteries.AssocList.instEmptyCollection = { emptyCollection := Batteries.AssocList.nil }
      @[simp]
      theorem Batteries.AssocList.empty_eq {α : Type u_1} {β : Type u_2} :
      = Batteries.AssocList.nil
      def Batteries.AssocList.isEmpty {α : Type u_1} {β : Type u_2} :

      O(1). Is the list empty?

      Equations
      • Batteries.AssocList.nil.isEmpty = true
      • x.isEmpty = false
      Instances For
        @[simp]
        theorem Batteries.AssocList.isEmpty_eq {α : Type u_1} {β : Type u_2} (l : Batteries.AssocList α β) :
        l.isEmpty = l.toList.isEmpty
        def Batteries.AssocList.length {α : Type u_1} {β : Type u_2} (L : Batteries.AssocList α β) :

        The number of entries in an AssocList.

        Equations
        Instances For
          @[simp]
          theorem Batteries.AssocList.length_nil {α : Type u_1} {β : Type u_2} :
          Batteries.AssocList.nil.length = 0
          @[simp]
          theorem Batteries.AssocList.length_cons :
          ∀ {α : Type u_1} {a : α} {β : Type u_2} {b : β} {t : Batteries.AssocList α β}, (Batteries.AssocList.cons a b t).length = t.length + 1
          theorem Batteries.AssocList.length_toList {α : Type u_1} {β : Type u_2} (l : Batteries.AssocList α β) :
          l.toList.length = l.length
          @[specialize #[]]
          def Batteries.AssocList.foldlM {m : Type u_1 → Type u_2} {δ : Type u_1} {α : Type u_3} {β : Type u_4} [Monad m] (f : δαβm δ) (init : δ) :
          Batteries.AssocList α βm δ

          O(n). Fold a monadic function over the list, from head to tail.

          Equations
          Instances For
            @[simp]
            theorem Batteries.AssocList.foldlM_eq {m : Type u_1 → Type u_2} {δ : Type u_1} {α : Type u_3} {β : Type u_4} [Monad m] (f : δαβm δ) (init : δ) (l : Batteries.AssocList α β) :
            Batteries.AssocList.foldlM f init l = List.foldlM (fun (d : δ) (x : α × β) => match x with | (a, b) => f d a b) init l.toList
            @[inline]
            def Batteries.AssocList.foldl {δ : Type u_1} {α : Type u_2} {β : Type u_3} (f : δαβδ) (init : δ) (as : Batteries.AssocList α β) :
            δ

            O(n). Fold a function over the list, from head to tail.

            Equations
            Instances For
              @[simp]
              theorem Batteries.AssocList.foldl_eq {δ : Type u_1} {α : Type u_2} {β : Type u_3} (f : δαβδ) (init : δ) (l : Batteries.AssocList α β) :
              Batteries.AssocList.foldl f init l = List.foldl (fun (d : δ) (x : α × β) => match x with | (a, b) => f d a b) init l.toList
              def Batteries.AssocList.toListTR {α : Type u_1} {β : Type u_2} (as : Batteries.AssocList α β) :
              List (α × β)

              Optimized version of toList.

              Equations
              Instances For
                @[specialize #[]]
                def Batteries.AssocList.forM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} [Monad m] (f : αβm PUnit) :

                O(n). Run monadic function f on all elements in the list, from head to tail.

                Equations
                Instances For
                  @[simp]
                  theorem Batteries.AssocList.forM_eq {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} [Monad m] (f : αβm PUnit) (l : Batteries.AssocList α β) :
                  Batteries.AssocList.forM f l = l.toList.forM fun (x : α × β) => match x with | (a, b) => f a b
                  def Batteries.AssocList.mapKey {α : Type u_1} {δ : Type u_2} {β : Type u_3} (f : αδ) :

                  O(n). Map a function f over the keys of the list.

                  Equations
                  Instances For
                    @[simp]
                    theorem Batteries.AssocList.toList_mapKey {α : Type u_1} {δ : Type u_2} {β : Type u_3} (f : αδ) (l : Batteries.AssocList α β) :
                    (Batteries.AssocList.mapKey f l).toList = List.map (fun (x : α × β) => match x with | (a, b) => (f a, b)) l.toList
                    @[simp]
                    theorem Batteries.AssocList.length_mapKey :
                    ∀ {α : Type u_1} {α_1 : Type u_2} {f : αα_1} {β : Type u_3} {l : Batteries.AssocList α β}, (Batteries.AssocList.mapKey f l).length = l.length
                    def Batteries.AssocList.mapVal {α : Type u_1} {β : Type u_2} {δ : Type u_3} (f : αβδ) :

                    O(n). Map a function f over the values of the list.

                    Equations
                    Instances For
                      @[simp]
                      theorem Batteries.AssocList.toList_mapVal {α : Type u_1} {β : Type u_2} {δ : Type u_3} (f : αβδ) (l : Batteries.AssocList α β) :
                      (Batteries.AssocList.mapVal f l).toList = List.map (fun (x : α × β) => match x with | (a, b) => (a, f a b)) l.toList
                      @[simp]
                      theorem Batteries.AssocList.length_mapVal :
                      ∀ {α : Type u_1} {β : Type u_2} {β_1 : Type u_3} {f : αββ_1} {l : Batteries.AssocList α β}, (Batteries.AssocList.mapVal f l).length = l.length
                      @[specialize #[]]
                      def Batteries.AssocList.findEntryP? {α : Type u_1} {β : Type u_2} (p : αβBool) :
                      Batteries.AssocList α βOption (α × β)

                      O(n). Returns the first entry in the list whose entry satisfies p.

                      Equations
                      Instances For
                        @[simp]
                        theorem Batteries.AssocList.findEntryP?_eq {α : Type u_1} {β : Type u_2} (p : αβBool) (l : Batteries.AssocList α β) :
                        Batteries.AssocList.findEntryP? p l = List.find? (fun (x : α × β) => match x with | (a, b) => p a b) l.toList
                        @[inline]
                        def Batteries.AssocList.findEntry? {α : Type u_1} {β : Type u_2} [BEq α] (a : α) (l : Batteries.AssocList α β) :
                        Option (α × β)

                        O(n). Returns the first entry in the list whose key is equal to a.

                        Equations
                        Instances For
                          @[simp]
                          theorem Batteries.AssocList.findEntry?_eq {α : Type u_1} {β : Type u_2} [BEq α] (a : α) (l : Batteries.AssocList α β) :
                          Batteries.AssocList.findEntry? a l = List.find? (fun (x : α × β) => x.fst == a) l.toList
                          def Batteries.AssocList.find? {α : Type u_1} {β : Type u_2} [BEq α] (a : α) :

                          O(n). Returns the first value in the list whose key is equal to a.

                          Equations
                          Instances For
                            theorem Batteries.AssocList.find?_eq_findEntry? {α : Type u_1} {β : Type u_2} [BEq α] (a : α) (l : Batteries.AssocList α β) :
                            @[simp]
                            theorem Batteries.AssocList.find?_eq {α : Type u_1} {β : Type u_2} [BEq α] (a : α) (l : Batteries.AssocList α β) :
                            Batteries.AssocList.find? a l = Option.map (fun (x : α × β) => x.snd) (List.find? (fun (x : α × β) => x.fst == a) l.toList)
                            @[specialize #[]]
                            def Batteries.AssocList.any {α : Type u_1} {β : Type u_2} (p : αβBool) :

                            O(n). Returns true if any entry in the list satisfies p.

                            Equations
                            Instances For
                              @[simp]
                              theorem Batteries.AssocList.any_eq {α : Type u_1} {β : Type u_2} (p : αβBool) (l : Batteries.AssocList α β) :
                              Batteries.AssocList.any p l = l.toList.any fun (x : α × β) => match x with | (a, b) => p a b
                              @[specialize #[]]
                              def Batteries.AssocList.all {α : Type u_1} {β : Type u_2} (p : αβBool) :

                              O(n). Returns true if every entry in the list satisfies p.

                              Equations
                              Instances For
                                @[simp]
                                theorem Batteries.AssocList.all_eq {α : Type u_1} {β : Type u_2} (p : αβBool) (l : Batteries.AssocList α β) :
                                Batteries.AssocList.all p l = l.toList.all fun (x : α × β) => match x with | (a, b) => p a b
                                def Batteries.AssocList.All {α : Type u_1} {β : Type u_2} (p : αβProp) (l : Batteries.AssocList α β) :

                                Returns true if every entry in the list satisfies p.

                                Equations
                                Instances For
                                  @[inline]
                                  def Batteries.AssocList.contains {α : Type u_1} {β : Type u_2} [BEq α] (a : α) (l : Batteries.AssocList α β) :

                                  O(n). Returns true if there is an element in the list whose key is equal to a.

                                  Equations
                                  Instances For
                                    @[simp]
                                    theorem Batteries.AssocList.contains_eq {α : Type u_1} {β : Type u_2} [BEq α] (a : α) (l : Batteries.AssocList α β) :
                                    Batteries.AssocList.contains a l = l.toList.any fun (x : α × β) => x.fst == a
                                    def Batteries.AssocList.replace {α : Type u_1} {β : Type u_2} [BEq α] (a : α) (b : β) :

                                    O(n). Replace the first entry in the list with key equal to a to have key a and value b.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    • Batteries.AssocList.replace a b Batteries.AssocList.nil = Batteries.AssocList.nil
                                    Instances For
                                      @[simp]
                                      theorem Batteries.AssocList.toList_replace {α : Type u_1} {β : Type u_2} [BEq α] (a : α) (b : β) (l : Batteries.AssocList α β) :
                                      (Batteries.AssocList.replace a b l).toList = List.replaceF (fun (x : α × β) => bif x.fst == a then some (a, b) else none) l.toList
                                      @[simp]
                                      theorem Batteries.AssocList.length_replace {α : Type u_1} :
                                      ∀ {β : Type u_2} {b : β} {l : Batteries.AssocList α β} [inst : BEq α] {a : α}, (Batteries.AssocList.replace a b l).length = l.length
                                      @[specialize #[]]
                                      def Batteries.AssocList.eraseP {α : Type u_1} {β : Type u_2} (p : αβBool) :

                                      O(n). Remove the first entry in the list with key equal to a.

                                      Equations
                                      Instances For
                                        @[simp]
                                        theorem Batteries.AssocList.toList_eraseP {α : Type u_1} {β : Type u_2} (p : αβBool) (l : Batteries.AssocList α β) :
                                        (Batteries.AssocList.eraseP p l).toList = List.eraseP (fun (x : α × β) => match x with | (a, b) => p a b) l.toList
                                        @[inline]
                                        def Batteries.AssocList.erase {α : Type u_1} {β : Type u_2} [BEq α] (a : α) (l : Batteries.AssocList α β) :

                                        O(n). Remove the first entry in the list with key equal to a.

                                        Equations
                                        Instances For
                                          @[simp]
                                          theorem Batteries.AssocList.toList_erase {α : Type u_1} {β : Type u_2} [BEq α] (a : α) (l : Batteries.AssocList α β) :
                                          (Batteries.AssocList.erase a l).toList = List.eraseP (fun (x : α × β) => x.fst == a) l.toList
                                          def Batteries.AssocList.modify {α : Type u_1} {β : Type u_2} [BEq α] (a : α) (f : αββ) :

                                          O(n). Replace the first entry a', b in the list with key equal to a to have key a and value f a' b.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          • Batteries.AssocList.modify a f Batteries.AssocList.nil = Batteries.AssocList.nil
                                          Instances For
                                            @[simp]
                                            theorem Batteries.AssocList.toList_modify {α : Type u_1} {β : Type u_2} {f : αββ} [BEq α] (a : α) (l : Batteries.AssocList α β) :
                                            (Batteries.AssocList.modify a f l).toList = List.replaceF (fun (x : α × β) => match x with | (k, v) => bif k == a then some (a, f k v) else none) l.toList
                                            @[simp]
                                            theorem Batteries.AssocList.length_modify {α : Type u_1} :
                                            ∀ {β : Type u_2} {f : αββ} {l : Batteries.AssocList α β} [inst : BEq α] {a : α}, (Batteries.AssocList.modify a f l).length = l.length
                                            @[specialize #[]]
                                            def Batteries.AssocList.forIn {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {δ : Type u_1} [Monad m] (as : Batteries.AssocList α β) (init : δ) (f : α × βδm (ForInStep δ)) :
                                            m δ

                                            The implementation of ForIn, which enables for (k, v) in aList do ... notation.

                                            Equations
                                            Instances For
                                              instance Batteries.AssocList.instForInProd {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} :
                                              ForIn m (Batteries.AssocList α β) (α × β)
                                              Equations
                                              • Batteries.AssocList.instForInProd = { forIn := fun {β_1 : Type ?u.28} [Monad m] => Batteries.AssocList.forIn }
                                              @[simp]
                                              theorem Batteries.AssocList.forIn_eq {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {δ : Type u_1} [Monad m] (l : Batteries.AssocList α β) (init : δ) (f : α × βδm (ForInStep δ)) :
                                              forIn l init f = forIn l.toList init f
                                              def Batteries.AssocList.pop? {α : Type u_1} {β : Type u_2} :

                                              Split the list into head and tail, if possible.

                                              Equations
                                              Instances For
                                                Equations
                                                instance Batteries.AssocList.instStreamProd {α : Type u_1} {β : Type u_2} :
                                                Stream (Batteries.AssocList α β) (α × β)
                                                Equations
                                                • Batteries.AssocList.instStreamProd = { next? := Batteries.AssocList.pop? }
                                                def List.toAssocList {α : Type u_1} {β : Type u_2} :
                                                List (α × β)Batteries.AssocList α β

                                                Converts a list into an AssocList. This is the inverse function to AssocList.toList.

                                                Equations
                                                Instances For
                                                  @[simp]
                                                  theorem List.toList_toAssocList {α : Type u_1} {β : Type u_2} (l : List (α × β)) :
                                                  l.toAssocList.toList = l
                                                  @[simp]
                                                  theorem Batteries.AssocList.toList_toAssocList {α : Type u_1} {β : Type u_2} (l : Batteries.AssocList α β) :
                                                  l.toList.toAssocList = l
                                                  @[simp]
                                                  theorem List.length_toAssocList {α : Type u_1} {β : Type u_2} (l : List (α × β)) :
                                                  l.toAssocList.length = l.length
                                                  def Batteries.AssocList.beq {α : Type u_1} {β : Type u_2} [BEq α] [BEq β] :

                                                  Implementation of == on AssocList.

                                                  Equations
                                                  Instances For
                                                    instance Batteries.AssocList.instBEq {α : Type u_1} {β : Type u_2} [BEq α] [BEq β] :

                                                    Boolean equality for AssocList. (This relation cares about the ordering of the key-value pairs.)

                                                    Equations
                                                    • Batteries.AssocList.instBEq = { beq := Batteries.AssocList.beq }
                                                    @[simp]
                                                    theorem Batteries.AssocList.beq_nil₂ {α : Type u_1} {β : Type u_2} [BEq α] [BEq β] :
                                                    (Batteries.AssocList.nil == Batteries.AssocList.nil) = true
                                                    @[simp]
                                                    theorem Batteries.AssocList.beq_nil_cons {α : Type u_1} {β : Type u_2} {a : α} {b : β} {t : Batteries.AssocList α β} [BEq α] [BEq β] :
                                                    (Batteries.AssocList.nil == Batteries.AssocList.cons a b t) = false
                                                    @[simp]
                                                    theorem Batteries.AssocList.beq_cons_nil {α : Type u_1} {β : Type u_2} {a : α} {b : β} {t : Batteries.AssocList α β} [BEq α] [BEq β] :
                                                    (Batteries.AssocList.cons a b t == Batteries.AssocList.nil) = false
                                                    @[simp]
                                                    theorem Batteries.AssocList.beq_cons₂ {α : Type u_1} {β : Type u_2} {a : α} {b : β} {t : Batteries.AssocList α β} {a' : α} {b' : β} {t' : Batteries.AssocList α β} [BEq α] [BEq β] :
                                                    (Batteries.AssocList.cons a b t == Batteries.AssocList.cons a' b' t') = (a == a' && b == b' && t == t')
                                                    instance Batteries.AssocList.instLawfulBEq {α : Type u_1} {β : Type u_2} [BEq α] [LawfulBEq α] [BEq β] [LawfulBEq β] :
                                                    Equations
                                                    • =
                                                    theorem Batteries.AssocList.beq_eq {α : Type u_1} {β : Type u_2} [BEq α] [BEq β] {l : Batteries.AssocList α β} {m : Batteries.AssocList α β} :
                                                    (l == m) = (l.toList == m.toList)