Documentation

Lean.Data.PersistentHashMap

inductive Lean.PersistentHashMap.Entry (α : Type u) (β : Type v) (σ : Type w) :
Type (max (max u v) w)
Instances For
    instance Lean.PersistentHashMap.instInhabitedEntry {α : Type u_1} {β : Type u_2} {σ : Type u_3} :
    Inhabited (Entry α β σ)
    Equations
      inductive Lean.PersistentHashMap.Node (α : Type u) (β : Type v) :
      Type (max u v)
      Instances For
        partial def Lean.PersistentHashMap.Node.isEmpty {α : Type u_1} {β : Type u_2} :
        Node α βBool
        instance Lean.PersistentHashMap.instInhabitedNode {α : Type u_1} {β : Type u_2} :
        Inhabited (Node α β)
        Equations
          @[reducible, inline]
          Equations
            Instances For
              @[reducible, inline]
              Equations
                Instances For
                  @[reducible, inline]
                  Equations
                    Instances For
                      @[reducible, inline]
                      Equations
                        Instances For
                          def Lean.PersistentHashMap.mkEmptyEntriesArray {α : Type u_1} {β : Type u_2} :
                          Array (Entry α β (Node α β))
                          Equations
                            Instances For
                              structure Lean.PersistentHashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] :
                              Type (max u v)
                              Instances For
                                @[reducible, inline]
                                abbrev Lean.PHashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] :
                                Type (max u v)
                                Equations
                                  Instances For
                                    def Lean.PersistentHashMap.empty {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] :
                                    Equations
                                      Instances For
                                        def Lean.PersistentHashMap.isEmpty {α : Type u_1} {β : Type u_2} {x✝ : BEq α} {x✝¹ : Hashable α} :
                                        Equations
                                          Instances For
                                            instance Lean.PersistentHashMap.instInhabited {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] :
                                            Equations
                                              def Lean.PersistentHashMap.mkEmptyEntries {α : Type u_1} {β : Type u_2} :
                                              Node α β
                                              Equations
                                                Instances For
                                                  @[reducible, inline]
                                                  Equations
                                                    Instances For
                                                      @[reducible, inline]
                                                      Equations
                                                        Instances For
                                                          @[reducible, inline]
                                                          Equations
                                                            Instances For
                                                              inductive Lean.PersistentHashMap.IsCollisionNode {α : Type u_1} {β : Type u_2} :
                                                              Node α βProp
                                                              Instances For
                                                                @[reducible, inline]
                                                                abbrev Lean.PersistentHashMap.CollisionNode (α : Type u_1) (β : Type u_2) :
                                                                Type (max 0 u_2 u_1)
                                                                Equations
                                                                  Instances For
                                                                    inductive Lean.PersistentHashMap.IsEntriesNode {α : Type u_1} {β : Type u_2} :
                                                                    Node α βProp
                                                                    Instances For
                                                                      @[reducible, inline]
                                                                      abbrev Lean.PersistentHashMap.EntriesNode (α : Type u_1) (β : Type u_2) :
                                                                      Type (max 0 u_2 u_1)
                                                                      Equations
                                                                        Instances For
                                                                          partial def Lean.PersistentHashMap.insertAtCollisionNodeAux {α : Type u_1} {β : Type u_2} [BEq α] :
                                                                          CollisionNode α βNatαβCollisionNode α β
                                                                          def Lean.PersistentHashMap.insertAtCollisionNode {α : Type u_1} {β : Type u_2} [BEq α] :
                                                                          CollisionNode α βαβCollisionNode α β
                                                                          Equations
                                                                            Instances For
                                                                              Equations
                                                                                Instances For
                                                                                  def Lean.PersistentHashMap.mkCollisionNode {α : Type u_1} {β : Type u_2} (k₁ : α) (v₁ : β) (k₂ : α) (v₂ : β) :
                                                                                  Node α β
                                                                                  Equations
                                                                                    Instances For
                                                                                      partial def Lean.PersistentHashMap.insertAux {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] :
                                                                                      Node α βUSizeUSizeαβNode α β
                                                                                      partial def Lean.PersistentHashMap.insertAux.traverse {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] (depth : USize) (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) (i : Nat) (entries : Node α β) :
                                                                                      Node α β
                                                                                      def Lean.PersistentHashMap.insert {α : Type u_1} {β : Type u_2} {x✝ : BEq α} {x✝¹ : Hashable α} :
                                                                                      PersistentHashMap α βαβPersistentHashMap α β
                                                                                      Equations
                                                                                        Instances For
                                                                                          partial def Lean.PersistentHashMap.findAtAux {α : Type u_1} {β : Type u_2} [BEq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) (i : Nat) (k : α) :
                                                                                          partial def Lean.PersistentHashMap.findAux {α : Type u_1} {β : Type u_2} [BEq α] :
                                                                                          Node α βUSizeαOption β
                                                                                          def Lean.PersistentHashMap.find? {α : Type u_1} {β : Type u_2} {x✝ : BEq α} {x✝¹ : Hashable α} :
                                                                                          PersistentHashMap α βαOption β
                                                                                          Equations
                                                                                            Instances For
                                                                                              instance Lean.PersistentHashMap.instGetElemOptionTrue {α : Type u_1} {β : Type u_2} {x✝ : BEq α} {x✝¹ : Hashable α} :
                                                                                              GetElem (PersistentHashMap α β) α (Option β) fun (x : PersistentHashMap α β) (x : α) => True
                                                                                              Equations
                                                                                                @[inline]
                                                                                                def Lean.PersistentHashMap.findD {α : Type u_1} {β : Type u_2} {x✝ : BEq α} {x✝¹ : Hashable α} (m : PersistentHashMap α β) (a : α) (b₀ : β) :
                                                                                                β
                                                                                                Equations
                                                                                                  Instances For
                                                                                                    @[inline]
                                                                                                    def Lean.PersistentHashMap.find! {α : Type u_1} {β : Type u_2} {x✝ : BEq α} {x✝¹ : Hashable α} [Inhabited β] (m : PersistentHashMap α β) (a : α) :
                                                                                                    β
                                                                                                    Equations
                                                                                                      Instances For
                                                                                                        partial def Lean.PersistentHashMap.findEntryAtAux {α : Type u_1} {β : Type u_2} [BEq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) (i : Nat) (k : α) :
                                                                                                        Option (α × β)
                                                                                                        partial def Lean.PersistentHashMap.findEntryAux {α : Type u_1} {β : Type u_2} [BEq α] :
                                                                                                        Node α βUSizeαOption (α × β)
                                                                                                        def Lean.PersistentHashMap.findEntry? {α : Type u_1} {β : Type u_2} {x✝ : BEq α} {x✝¹ : Hashable α} :
                                                                                                        PersistentHashMap α βαOption (α × β)
                                                                                                        Equations
                                                                                                          Instances For
                                                                                                            partial def Lean.PersistentHashMap.containsAtAux {α : Type u_1} {β : Type u_2} [BEq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) (i : Nat) (k : α) :
                                                                                                            partial def Lean.PersistentHashMap.containsAux {α : Type u_1} {β : Type u_2} [BEq α] :
                                                                                                            Node α βUSizeαBool
                                                                                                            def Lean.PersistentHashMap.contains {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] :
                                                                                                            PersistentHashMap α βαBool
                                                                                                            Equations
                                                                                                              Instances For
                                                                                                                partial def Lean.PersistentHashMap.isUnaryEntries {α : Type u_1} {β : Type u_2} (a : Array (Entry α β (Node α β))) (i : Nat) (acc : Option (α × β)) :
                                                                                                                Option (α × β)
                                                                                                                def Lean.PersistentHashMap.isUnaryNode {α : Type u_1} {β : Type u_2} :
                                                                                                                Node α βOption (α × β)
                                                                                                                Equations
                                                                                                                  Instances For
                                                                                                                    partial def Lean.PersistentHashMap.eraseAux {α : Type u_1} {β : Type u_2} [BEq α] :
                                                                                                                    Node α βUSizeαNode α β
                                                                                                                    def Lean.PersistentHashMap.erase {α : Type u_1} {β : Type u_2} {x✝ : BEq α} {x✝¹ : Hashable α} :
                                                                                                                    PersistentHashMap α βαPersistentHashMap α β
                                                                                                                    Equations
                                                                                                                      Instances For
                                                                                                                        partial def Lean.PersistentHashMap.foldlMAux {m : Type w → Type w'} [Monad m] {σ : Type w} {α : Type u_1} {β : Type u_2} (f : σαβm σ) :
                                                                                                                        Node α βσm σ
                                                                                                                        partial def Lean.PersistentHashMap.foldlMAux.traverse {m : Type w → Type w'} [Monad m] {σ : Type w} {α : Type u_1} {β : Type u_2} (f : σαβm σ) (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) (i : Nat) (acc : σ) :
                                                                                                                        m σ
                                                                                                                        def Lean.PersistentHashMap.foldlM {m : Type w → Type w'} [Monad m] {σ : Type w} {α : Type u_1} {β : Type u_2} {x✝ : BEq α} {x✝¹ : Hashable α} (map : PersistentHashMap α β) (f : σαβm σ) (init : σ) :
                                                                                                                        m σ
                                                                                                                        Equations
                                                                                                                          Instances For
                                                                                                                            def Lean.PersistentHashMap.forM {m : Type w → Type w'} [Monad m] {α : Type u_1} {β : Type u_2} {x✝ : BEq α} {x✝¹ : Hashable α} (map : PersistentHashMap α β) (f : αβm PUnit) :
                                                                                                                            Equations
                                                                                                                              Instances For
                                                                                                                                def Lean.PersistentHashMap.foldl {σ : Type w} {α : Type u_1} {β : Type u_2} {x✝ : BEq α} {x✝¹ : Hashable α} (map : PersistentHashMap α β) (f : σαβσ) (init : σ) :
                                                                                                                                σ
                                                                                                                                Equations
                                                                                                                                  Instances For
                                                                                                                                    def Lean.PersistentHashMap.forIn {m : Type w → Type w'} {σ : Type w} {α : Type u_1} {β : Type u_2} {x✝ : BEq α} {x✝¹ : Hashable α} [Monad m] (map : PersistentHashMap α β) (init : σ) (f : α × βσm (ForInStep σ)) :
                                                                                                                                    m σ
                                                                                                                                    Equations
                                                                                                                                      Instances For
                                                                                                                                        instance Lean.PersistentHashMap.instForInProd {m : Type w → Type w'} {α : Type u_1} {β : Type u_2} {x✝ : BEq α} {x✝¹ : Hashable α} :
                                                                                                                                        ForIn m (PersistentHashMap α β) (α × β)
                                                                                                                                        Equations
                                                                                                                                          partial def Lean.PersistentHashMap.mapMAux {α : Type u} {β : Type v} {σ : Type u} {m : Type u → Type w} [Monad m] (f : βm σ) (n : Node α β) :
                                                                                                                                          m (Node α σ)
                                                                                                                                          def Lean.PersistentHashMap.mapM {α : Type u} {β : Type v} {σ : Type u} {m : Type u → Type w} [Monad m] {x✝ : BEq α} {x✝¹ : Hashable α} (pm : PersistentHashMap α β) (f : βm σ) :
                                                                                                                                          Equations
                                                                                                                                            Instances For
                                                                                                                                              def Lean.PersistentHashMap.map {α : Type u} {β : Type v} {σ : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} (pm : PersistentHashMap α β) (f : βσ) :
                                                                                                                                              Equations
                                                                                                                                                Instances For
                                                                                                                                                  def Lean.PersistentHashMap.toList {α : Type u_1} {β : Type u_2} {x✝ : BEq α} {x✝¹ : Hashable α} (m : PersistentHashMap α β) :
                                                                                                                                                  List (α × β)
                                                                                                                                                  Equations
                                                                                                                                                    Instances For
                                                                                                                                                      def Lean.PersistentHashMap.toArray {α : Type u_1} {β : Type u_2} {x✝ : BEq α} {x✝¹ : Hashable α} (m : PersistentHashMap α β) :
                                                                                                                                                      Array (α × β)
                                                                                                                                                      Equations
                                                                                                                                                        Instances For
                                                                                                                                                          • numNodes : Nat
                                                                                                                                                          • numNull : Nat
                                                                                                                                                          • numCollisions : Nat
                                                                                                                                                          • maxDepth : Nat
                                                                                                                                                          Instances For
                                                                                                                                                            partial def Lean.PersistentHashMap.collectStats {α : Type u_1} {β : Type u_2} :
                                                                                                                                                            Node α βStatsNatStats
                                                                                                                                                            def Lean.PersistentHashMap.stats {α : Type u_1} {β : Type u_2} {x✝ : BEq α} {x✝¹ : Hashable α} (m : PersistentHashMap α β) :
                                                                                                                                                            Equations
                                                                                                                                                              Instances For