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 : USize.toNat i < Array.size data.val) :
    Equations
    Instances For
      structure Lean.HashMapImp (α : Type u) (β : Type v) :
      Type (max u v)
      Instances For
        def Lean.mkHashMapImp {α : Type u} {β : Type v} (capacity : optParam Nat 8) :
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[inline]
          def Lean.HashMapImp.reinsertAux {α : Type u} {β : Type v} (hashFn : αUInt64) (data : Lean.HashMapBucket α β) (a : α) (b : β) :
          Equations
          • One or more equations did not get rendered due to their size.
          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
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          def Lean.HashMapImp.find? {α : Type u} {β : Type v} [beq : BEq α] [Hashable α] (m : Lean.HashMapImp α β) (a : α) :
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            def Lean.HashMapImp.contains {α : 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
                              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
                                • One or more equations did not get rendered due to their size.
                                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
                                    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
                                        def Lean.HashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] :
                                        Type (max 0 u v)
                                        Equations
                                        Instances For
                                          def Lean.mkHashMap {α : Type u} {β : Type v} [BEq α] [Hashable α] (capacity : optParam Nat 8) :
                                          Equations
                                          Instances For
                                            instance Lean.HashMap.instInhabitedHashMap {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] :
                                            Equations
                                            • Lean.HashMap.instInhabitedHashMap = { default := Lean.mkHashMap }
                                            Equations
                                            • Lean.HashMap.instEmptyCollectionHashMap = { emptyCollection := Lean.mkHashMap }
                                            @[inline]
                                            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
                                              • One or more equations did not get rendered due to their size.
                                              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 flad indicating whether an existing entry has been replaced with a -> b.

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                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
                                                        Instances For
                                                          @[inline]
                                                          def Lean.HashMap.find! {α : Type u} {β : Type v} :
                                                          {x : BEq α} → {x_1 : Hashable α} → [inst : Inhabited β] → Lean.HashMap α βαβ
                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For
                                                            instance Lean.HashMap.instGetElemHashMapOptionTrue {α : Type u} {β : Type v} :
                                                            {x : BEq α} → {x_1 : Hashable α} → GetElem (Lean.HashMap α β) α (Option β) fun x x => True
                                                            Equations
                                                            @[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
                                                                    • Lean.HashMap.size m = match m with | { val := { size := sz, buckets := buckets }, property := property } => sz
                                                                    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
                                                                            Instances For
                                                                              def Lean.HashMap.ofList {α : Type u} {β : Type v} :
                                                                              {x : BEq α} → {x_1 : Hashable α} → List (α × β)Lean.HashMap α β

                                                                              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} :
                                                                                {x : BEq α} → {x_1 : Hashable α} → List (α × β)(βββ) → Lean.HashMap α β

                                                                                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