Documentation

Lean.Data.HashMap

def Lean.HashMapBucket (α : Type u) (β : Type v) :
Type (max 0 u v)
Equations
Instances For
    def Lean.HashMapBucket.update {α : Type u} {β : Type v} (data : Lean.HashMapBucket α β) (i : USize) (d : Lean.AssocList α β) (h : i.toNat < data.val.size) :
    Equations
    • data.update i d h = data.val.uset i d h,
    Instances For
      @[simp]
      theorem Lean.HashMapBucket.size_update {α : Type u} {β : Type v} (data : Lean.HashMapBucket α β) (i : USize) (d : Lean.AssocList α β) (h : i.toNat < data.val.size) :
      (data.update i d h).val.size = data.val.size
      @[deprecated Std.HashMap.Raw]
      structure Lean.HashMapImp (α : Type u) (β : Type v) :
      Type (max u v)
      Instances For
        @[deprecated Std.HashMap.Raw.empty]
        def Lean.mkHashMapImp {α : Type u} {β : Type v} (capacity : optParam Nat 8) :
        Equations
        Instances For
          @[inline]
          def Lean.HashMapImp.reinsertAux {α : Type u} {β : Type v} (hashFn : αUInt64) (data : Lean.HashMapBucket α β) (a : α) (b : β) :
          Equations
          Instances For
            @[inline]
            def Lean.HashMapImp.foldBucketsM {α : Type u} {β : Type v} {δ : Type w} {m : Type w → Type w} [Monad m] (data : Lean.HashMapBucket α β) (d : δ) (f : δαβm δ) :
            m δ
            Equations
            Instances For
              @[inline]
              def Lean.HashMapImp.foldBuckets {α : Type u} {β : Type v} {δ : Type w} (data : Lean.HashMapBucket α β) (d : δ) (f : δαβδ) :
              δ
              Equations
              Instances For
                @[inline]
                def Lean.HashMapImp.foldM {α : Type u} {β : Type v} {δ : Type w} {m : Type w → Type w} [Monad m] (f : δαβm δ) (d : δ) (h : Lean.HashMapImp α β) :
                m δ
                Equations
                Instances For
                  @[inline]
                  def Lean.HashMapImp.fold {α : Type u} {β : Type v} {δ : Type w} (f : δαβδ) (d : δ) (m : Lean.HashMapImp α β) :
                  δ
                  Equations
                  Instances For
                    @[inline]
                    def Lean.HashMapImp.forBucketsM {α : Type u} {β : Type v} {m : Type w → Type w} [Monad m] (data : Lean.HashMapBucket α β) (f : αβm PUnit) :
                    Equations
                    Instances For
                      @[inline]
                      def Lean.HashMapImp.forM {α : Type u} {β : Type v} {m : Type w → Type w} [Monad m] (f : αβm PUnit) (h : Lean.HashMapImp α β) :
                      Equations
                      Instances For
                        def Lean.HashMapImp.findEntry? {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : Lean.HashMapImp α β) (a : α) :
                        Option (α × β)
                        Equations
                        Instances For
                          def Lean.HashMapImp.find? {α : Type u} {β : Type v} [beq : BEq α] [Hashable α] (m : Lean.HashMapImp α β) (a : α) :
                          Equations
                          Instances For
                            def Lean.HashMapImp.contains {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : Lean.HashMapImp α β) (a : α) :
                            Equations
                            Instances For
                              @[irreducible]
                              def Lean.HashMapImp.moveEntries {α : Type u} {β : Type v} [Hashable α] (i : Nat) (source : Array (Lean.AssocList α β)) (target : Lean.HashMapBucket α β) :
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                def Lean.HashMapImp.expand {α : Type u} {β : Type v} [Hashable α] (size : Nat) (buckets : Lean.HashMapBucket α β) :
                                Equations
                                Instances For
                                  @[inline]
                                  def Lean.HashMapImp.insert {α : Type u} {β : Type v} [beq : BEq α] [Hashable α] (m : Lean.HashMapImp α β) (a : α) (b : β) :
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    @[inline]
                                    def Lean.HashMapImp.insertIfNew {α : Type u} {β : Type v} [beq : BEq α] [Hashable α] (m : Lean.HashMapImp α β) (a : α) (b : β) :
                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      def Lean.HashMapImp.erase {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : Lean.HashMapImp α β) (a : α) :
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        inductive Lean.HashMapImp.WellFormed {α : Type u} {β : Type v} [BEq α] [Hashable α] :
                                        Instances For
                                          @[deprecated Std.HashMap]
                                          def Lean.HashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] :
                                          Type (max 0 u v)
                                          Equations
                                          Instances For
                                            @[deprecated Std.HashMap.empty]
                                            def Lean.mkHashMap {α : Type u} {β : Type v} [BEq α] [Hashable α] (capacity : optParam Nat 8) :
                                            Equations
                                            Instances For
                                              instance Lean.HashMap.instInhabited {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] :
                                              Equations
                                              • Lean.HashMap.instInhabited = { default := Lean.mkHashMap }
                                              instance Lean.HashMap.instEmptyCollection {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] :
                                              Equations
                                              • Lean.HashMap.instEmptyCollection = { emptyCollection := Lean.mkHashMap }
                                              @[inline, deprecated Std.HashMap.empty]
                                              def Lean.HashMap.empty {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] :
                                              Equations
                                              • Lean.HashMap.empty = Lean.mkHashMap
                                              Instances For
                                                def Lean.HashMap.insert {α : Type u} {β : Type v} :
                                                {x : BEq α} → {x_1 : Hashable α} → Lean.HashMap α βαβLean.HashMap α β
                                                Equations
                                                Instances For
                                                  def Lean.HashMap.insert' {α : Type u} {β : Type v} :
                                                  {x : BEq α} → {x_1 : Hashable α} → Lean.HashMap α βαβLean.HashMap α β × Bool

                                                  Similar to insert, but also returns a Boolean flag indicating whether an existing entry has been replaced with a -> b.

                                                  Equations
                                                  • Lean.HashMap.insert' m_2, hw a b = match h : m_2.insert a b with | (m', replaced) => (m', , replaced)
                                                  Instances For
                                                    def Lean.HashMap.insertIfNew {α : Type u} {β : Type v} :
                                                    {x : BEq α} → {x_1 : Hashable α} → Lean.HashMap α βαβLean.HashMap α β × Option β

                                                    Similar to insert, but returns some old if the map already had an entry α → old. If the result is some old, the the resulting map is equal to m.

                                                    Equations
                                                    Instances For
                                                      @[inline]
                                                      def Lean.HashMap.erase {α : Type u} {β : Type v} :
                                                      {x : BEq α} → {x_1 : Hashable α} → Lean.HashMap α βαLean.HashMap α β
                                                      Equations
                                                      Instances For
                                                        @[inline]
                                                        def Lean.HashMap.findEntry? {α : Type u} {β : Type v} :
                                                        {x : BEq α} → {x_1 : Hashable α} → Lean.HashMap α βαOption (α × β)
                                                        Equations
                                                        Instances For
                                                          @[inline]
                                                          def Lean.HashMap.find? {α : Type u} {β : Type v} :
                                                          {x : BEq α} → {x_1 : Hashable α} → Lean.HashMap α βαOption β
                                                          Equations
                                                          Instances For
                                                            @[inline]
                                                            def Lean.HashMap.findD {α : Type u} {β : Type v} :
                                                            {x : BEq α} → {x_1 : Hashable α} → Lean.HashMap α βαββ
                                                            Equations
                                                            • m.findD a b₀ = (m.find? a).getD b₀
                                                            Instances For
                                                              @[inline]
                                                              def Lean.HashMap.find! {α : Type u} {β : Type v} :
                                                              {x : BEq α} → {x_1 : Hashable α} → [inst : Inhabited β] → Lean.HashMap α βαβ
                                                              Equations
                                                              • m.find! a = match m.find? a with | some b => b | none => panicWithPosWithDecl "Lean.Data.HashMap" "Lean.HashMap.find!" 223 14 "key is not in the map"
                                                              Instances For
                                                                instance Lean.HashMap.instGetElemOptionTrue {α : Type u} {β : Type v} :
                                                                {x : BEq α} → {x_1 : Hashable α} → GetElem (Lean.HashMap α β) α (Option β) fun (x : Lean.HashMap α β) (x : α) => True
                                                                Equations
                                                                • Lean.HashMap.instGetElemOptionTrue = { getElem := fun (m : Lean.HashMap α β) (k : α) (x_1 : True) => m.find? k }
                                                                @[inline]
                                                                def Lean.HashMap.contains {α : Type u} {β : Type v} :
                                                                {x : BEq α} → {x_1 : Hashable α} → Lean.HashMap α βαBool
                                                                Equations
                                                                Instances For
                                                                  @[inline]
                                                                  def Lean.HashMap.foldM {α : Type u} {β : Type v} :
                                                                  {x : BEq α} → {x_1 : Hashable α} → {δ : Type w} → {m : Type w → Type w} → [inst : Monad m] → (δαβm δ)δLean.HashMap α βm δ
                                                                  Equations
                                                                  Instances For
                                                                    @[inline]
                                                                    def Lean.HashMap.fold {α : Type u} {β : Type v} :
                                                                    {x : BEq α} → {x_1 : Hashable α} → {δ : Type w} → (δαβδ)δLean.HashMap α βδ
                                                                    Equations
                                                                    Instances For
                                                                      @[inline]
                                                                      def Lean.HashMap.forM {α : Type u} {β : Type v} :
                                                                      {x : BEq α} → {x_1 : Hashable α} → {m : Type w → Type w} → [inst : Monad m] → (αβm PUnit)Lean.HashMap α βm PUnit
                                                                      Equations
                                                                      Instances For
                                                                        @[inline]
                                                                        def Lean.HashMap.size {α : Type u} {β : Type v} :
                                                                        {x : BEq α} → {x_1 : Hashable α} → Lean.HashMap α βNat
                                                                        Equations
                                                                        Instances For
                                                                          @[inline]
                                                                          def Lean.HashMap.isEmpty {α : Type u} {β : Type v} :
                                                                          {x : BEq α} → {x_1 : Hashable α} → Lean.HashMap α βBool
                                                                          Equations
                                                                          Instances For
                                                                            def Lean.HashMap.toList {α : Type u} {β : Type v} :
                                                                            {x : BEq α} → {x_1 : Hashable α} → Lean.HashMap α βList (α × β)
                                                                            Equations
                                                                            Instances For
                                                                              def Lean.HashMap.toArray {α : Type u} {β : Type v} :
                                                                              {x : BEq α} → {x_1 : Hashable α} → Lean.HashMap α βArray (α × β)
                                                                              Equations
                                                                              Instances For
                                                                                def Lean.HashMap.numBuckets {α : Type u} {β : Type v} :
                                                                                {x : BEq α} → {x_1 : Hashable α} → Lean.HashMap α βNat
                                                                                Equations
                                                                                • m.numBuckets = m.val.buckets.val.size
                                                                                Instances For
                                                                                  @[deprecated Std.HashMap.ofList]
                                                                                  def Lean.HashMap.ofList {α : Type u} {β : Type v} [BEq α] [Hashable α] (l : List (α × β)) :

                                                                                  Builds a HashMap from a list of key-value pairs. Values of duplicated keys are replaced by their respective last occurrences.

                                                                                  Equations
                                                                                  Instances For
                                                                                    def Lean.HashMap.ofListWith {α : Type u} {β : Type v} [BEq α] [Hashable α] (l : List (α × β)) (f : βββ) :

                                                                                    Variant of ofList which accepts a function that combines values of duplicated keys.

                                                                                    Equations
                                                                                    • One or more equations did not get rendered due to their size.
                                                                                    Instances For