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_1 : Type u_2} → Inhabited (Lean.AssocList a a_1)
    Equations
    • Lean.instInhabitedAssocList = { default := Lean.AssocList.nil }
    @[inline, reducible]
    abbrev Lean.AssocList.empty {α : Type u} {β : Type v} :
    Equations
    • Lean.AssocList.empty = Lean.AssocList.nil
    Instances For
      Equations
      • Lean.AssocList.instEmptyCollectionAssocList = { emptyCollection := Lean.AssocList.empty }
      @[inline, reducible]
      abbrev Lean.AssocList.insert {α : Type u} {β : Type v} (m : Lean.AssocList α β) (k : α) (v : β) :
      Equations
      Instances For
        def Lean.AssocList.isEmpty {α : Type u} {β : Type v} :
        Equations
        Instances For
          @[specialize #[]]
          def Lean.AssocList.foldlM {α : Type u} {β : Type v} {δ : Type w} {m : Type w → Type w} [Monad m] (f : δαβm δ) (init : δ) :
          Lean.AssocList α βm δ
          Equations
          Instances For
            @[inline]
            def Lean.AssocList.foldl {α : Type u} {β : Type v} {δ : Type w} (f : δαβδ) (init : δ) (as : Lean.AssocList α β) :
            δ
            Equations
            Instances For
              def Lean.AssocList.toList {α : Type u} {β : Type v} (as : Lean.AssocList α β) :
              List (α × β)
              Equations
              Instances For
                @[specialize #[]]
                def Lean.AssocList.forM {α : Type u} {β : Type v} {m : Type w → Type w} [Monad m] (f : αβm PUnit) :
                Lean.AssocList α βm PUnit
                Equations
                Instances For
                  def Lean.AssocList.mapKey {α : Type u} {β : Type v} {δ : Type w} (f : αδ) :
                  Equations
                  Instances For
                    def Lean.AssocList.mapVal {α : Type u} {β : Type v} {δ : Type w} (f : βδ) :
                    Equations
                    Instances For
                      def Lean.AssocList.findEntry? {α : Type u} {β : Type v} [BEq α] (a : α) :
                      Lean.AssocList α βOption (α × β)
                      Equations
                      Instances For
                        def Lean.AssocList.find? {α : Type u} {β : Type v} [BEq α] (a : α) :
                        Lean.AssocList α βOption β
                        Equations
                        Instances For
                          def Lean.AssocList.contains {α : Type u} {β : Type v} [BEq α] (a : α) :
                          Equations
                          Instances For
                            def Lean.AssocList.replace {α : Type u} {β : Type v} [BEq α] (a : α) (b : β) :
                            Equations
                            Instances For
                              def Lean.AssocList.erase {α : Type u} {β : Type v} [BEq α] (a : α) :
                              Equations
                              Instances For
                                def Lean.AssocList.any {α : Type u} {β : Type v} (p : αβBool) :
                                Equations
                                Instances For
                                  def Lean.AssocList.all {α : Type u} {β : Type v} (p : αβBool) :
                                  Equations
                                  Instances For
                                    @[inline]
                                    def Lean.AssocList.forIn {α : Type u} {β : Type v} {δ : Type w} {m : Type w → Type w'} [Monad m] (as : Lean.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 δ)) :
                                      δLean.AssocList α βm δ
                                      Equations
                                      Instances For
                                        instance Lean.AssocList.instForInAssocListProd {α : Type u} {β : Type v} {m : Type w → Type w} :
                                        ForIn m (Lean.AssocList α β) (α × β)
                                        Equations
                                        • Lean.AssocList.instForInAssocListProd = { forIn := fun {β} [Monad m] => Lean.AssocList.forIn }
                                        def List.toAssocList' {α : Type u} {β : Type v} :
                                        List (α × β)Lean.AssocList α β
                                        Equations
                                        Instances For