Documentation

Lean.Data.AssocList

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

List-like type to avoid extra level of indirection

Instances For
    instance Lean.instInhabitedAssocList {a✝ : Type u_1} {a✝¹ : Type u_2} :
    Inhabited (AssocList a✝ a✝¹)
    Equations
      @[reducible, inline]
      abbrev Lean.AssocList.empty {α : Type u} {β : Type v} :
      AssocList α β
      Equations
        Instances For
          Equations
            @[reducible, inline]
            abbrev Lean.AssocList.insertNew {α : Type u} {β : Type v} (m : AssocList α β) (k : α) (v : β) :
            AssocList α β
            Equations
              Instances For
                def Lean.AssocList.isEmpty {α : Type u} {β : Type v} :
                AssocList α βBool
                Equations
                  Instances For
                    @[specialize #[]]
                    def Lean.AssocList.foldlM {α : Type u} {β : Type v} {δ : Type w} {m : Type w → Type w} [Monad m] (f : δαβm δ) (init : δ) :
                    AssocList α βm δ
                    Equations
                      Instances For
                        @[inline]
                        def Lean.AssocList.foldl {α : Type u} {β : Type v} {δ : Type w} (f : δαβδ) (init : δ) (as : AssocList α β) :
                        δ
                        Equations
                          Instances For
                            def Lean.AssocList.toList {α : Type u} {β : Type v} (as : AssocList α β) :
                            List (α × β)
                            Equations
                              Instances For
                                @[specialize #[]]
                                def Lean.AssocList.forM {α : Type u} {β : Type v} {m : Type w → Type w} [Monad m] (f : αβm PUnit) :
                                AssocList α βm PUnit
                                Equations
                                  Instances For
                                    def Lean.AssocList.mapKey {α : Type u} {β : Type v} {δ : Type w} (f : αδ) :
                                    AssocList α βAssocList δ β
                                    Equations
                                      Instances For
                                        def Lean.AssocList.mapVal {α : Type u} {β : Type v} {δ : Type w} (f : βδ) :
                                        AssocList α βAssocList α δ
                                        Equations
                                          Instances For
                                            def Lean.AssocList.findEntry? {α : Type u} {β : Type v} [BEq α] (a : α) :
                                            AssocList α βOption (α × β)
                                            Equations
                                              Instances For
                                                def Lean.AssocList.find? {α : Type u} {β : Type v} [BEq α] (a : α) :
                                                AssocList α βOption β
                                                Equations
                                                  Instances For
                                                    def Lean.AssocList.contains {α : Type u} {β : Type v} [BEq α] (a : α) :
                                                    AssocList α βBool
                                                    Equations
                                                      Instances For
                                                        def Lean.AssocList.replace {α : Type u} {β : Type v} [BEq α] (a : α) (b : β) :
                                                        AssocList α βAssocList α β
                                                        Equations
                                                          Instances For
                                                            def Lean.AssocList.insert {α : Type u} {β : Type v} [BEq α] (m : AssocList α β) (k : α) (v : β) :
                                                            AssocList α β
                                                            Equations
                                                              Instances For
                                                                def Lean.AssocList.erase {α : Type u} {β : Type v} [BEq α] (a : α) :
                                                                AssocList α βAssocList α β
                                                                Equations
                                                                  Instances For
                                                                    def Lean.AssocList.any {α : Type u} {β : Type v} (p : αβBool) :
                                                                    AssocList α βBool
                                                                    Equations
                                                                      Instances For
                                                                        def Lean.AssocList.all {α : Type u} {β : Type v} (p : αβBool) :
                                                                        AssocList α βBool
                                                                        Equations
                                                                          Instances For
                                                                            @[inline]
                                                                            def Lean.AssocList.forIn {α : Type u} {β : Type v} {δ : Type w} {m : Type w → Type w'} [Monad m] (as : AssocList α β) (init : δ) (f : α × βδm (ForInStep δ)) :
                                                                            m δ
                                                                            Equations
                                                                              Instances For
                                                                                @[specialize #[]]
                                                                                def Lean.AssocList.forIn.loop {α : Type u} {β : Type v} {δ : Type w} {m : Type w → Type w'} [Monad m] (f : α × βδm (ForInStep δ)) :
                                                                                δAssocList α βm δ
                                                                                Equations
                                                                                  Instances For
                                                                                    instance Lean.AssocList.instForInProd {α : Type u} {β : Type v} {m : Type w → Type w} :
                                                                                    ForIn m (AssocList α β) (α × β)
                                                                                    Equations
                                                                                      def List.toAssocList' {α : Type u} {β : Type v} :
                                                                                      List (α × β)Lean.AssocList α β
                                                                                      Equations
                                                                                        Instances For