Documentation

Lean.Data.PersistentHashMap

inductive Lean.PersistentHashMap.Entry (α : Type u) (β : Type v) (σ : Type w) :
Type (max (max u v) w)
Instances For
    Equations
    • Lean.PersistentHashMap.instInhabitedEntry = { default := Lean.PersistentHashMap.Entry.null }
    inductive Lean.PersistentHashMap.Node (α : Type u) (β : Type v) :
    Type (max u v)
    Instances For
      Equations
      @[inline, reducible]
      Equations
      Instances For
        @[inline, reducible]
        Equations
        Instances For
          @[inline, reducible]
          Equations
          Instances For
            Equations
            Instances For
              structure Lean.PersistentHashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] :
              Type (max u v)
              Instances For
                @[inline, reducible]
                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} [BEq α] [Hashable α] (m : Lean.PersistentHashMap α β) :
                    Equations
                    Instances For
                      Equations
                      Equations
                      Instances For
                        @[inline, reducible]
                        Equations
                        Instances For
                          @[inline, reducible]
                          Equations
                          Instances For
                            @[inline, reducible]
                            Equations
                            Instances For
                              Instances For
                                @[inline, reducible]
                                abbrev Lean.PersistentHashMap.CollisionNode (α : Type u_1) (β : Type u_2) :
                                Type (max 0 u_2 u_1)
                                Equations
                                Instances For
                                  @[inline, reducible]
                                  abbrev Lean.PersistentHashMap.EntriesNode (α : Type u_1) (β : Type u_2) :
                                  Type (max 0 u_2 u_1)
                                  Equations
                                  Instances For
                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      def Lean.PersistentHashMap.mkCollisionNode {α : Type u_1} {β : Type u_2} (k₁ : α) (v₁ : β) (k₂ : α) (v₂ : β) :
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        partial def Lean.PersistentHashMap.insertAux {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] :
                                        partial def Lean.PersistentHashMap.insertAux.traverse {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] (depth : USize) (keys : Array α) (vals : Array β) (heq : Array.size keys = Array.size vals) (i : Nat) (entries : Lean.PersistentHashMap.Node α β) :
                                        def Lean.PersistentHashMap.insert {α : Type u_1} {β : Type u_2} :
                                        {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashMap α βαβLean.PersistentHashMap α β
                                        Equations
                                        Instances For
                                          partial def Lean.PersistentHashMap.findAtAux {α : Type u_1} {β : Type u_2} [BEq α] (keys : Array α) (vals : Array β) (heq : Array.size keys = Array.size vals) (i : Nat) (k : α) :
                                          partial def Lean.PersistentHashMap.findAux {α : Type u_1} {β : Type u_2} [BEq α] :
                                          Lean.PersistentHashMap.Node α βUSizeαOption β
                                          def Lean.PersistentHashMap.find? {α : Type u_1} {β : Type u_2} :
                                          {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashMap α βαOption β
                                          Equations
                                          Instances For
                                            instance Lean.PersistentHashMap.instGetElemPersistentHashMapOptionTrue {α : Type u_1} {β : Type u_2} :
                                            {x : BEq α} → {x_1 : Hashable α} → GetElem (Lean.PersistentHashMap α β) α (Option β) fun x x => True
                                            Equations
                                            @[inline]
                                            def Lean.PersistentHashMap.findD {α : Type u_1} {β : Type u_2} :
                                            {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashMap α βαββ
                                            Equations
                                            Instances For
                                              @[inline]
                                              def Lean.PersistentHashMap.find! {α : Type u_1} {β : Type u_2} :
                                              {x : BEq α} → {x_1 : Hashable α} → [inst : Inhabited β] → Lean.PersistentHashMap α βαβ
                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                partial def Lean.PersistentHashMap.findEntryAtAux {α : Type u_1} {β : Type u_2} [BEq α] (keys : Array α) (vals : Array β) (heq : Array.size keys = Array.size vals) (i : Nat) (k : α) :
                                                Option (α × β)
                                                partial def Lean.PersistentHashMap.findEntryAux {α : Type u_1} {β : Type u_2} [BEq α] :
                                                Lean.PersistentHashMap.Node α βUSizeαOption (α × β)
                                                def Lean.PersistentHashMap.findEntry? {α : Type u_1} {β : Type u_2} :
                                                {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashMap α βαOption (α × β)
                                                Equations
                                                Instances For
                                                  partial def Lean.PersistentHashMap.containsAtAux {α : Type u_1} {β : Type u_2} [BEq α] (keys : Array α) (vals : Array β) (heq : Array.size keys = Array.size vals) (i : Nat) (k : α) :
                                                  partial def Lean.PersistentHashMap.containsAux {α : Type u_1} {β : Type u_2} [BEq α] :
                                                  def Lean.PersistentHashMap.contains {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] :
                                                  Lean.PersistentHashMap α βαBool
                                                  Equations
                                                  Instances For
                                                    partial def Lean.PersistentHashMap.isUnaryEntries {α : Type u_1} {β : Type u_2} (a : Array (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β))) (i : Nat) (acc : Option (α × β)) :
                                                    Option (α × β)
                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      def Lean.PersistentHashMap.erase {α : Type u_1} {β : Type u_2} :
                                                      {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashMap α βαLean.PersistentHashMap α β
                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        partial def Lean.PersistentHashMap.foldlMAux {m : Type w → Type w'} [Monad m] {σ : Type w} {α : Type u_1} {β : Type u_2} (f : σαβm σ) :
                                                        Lean.PersistentHashMap.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 : Array.size keys = Array.size vals) (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_1 : Hashable α} → Lean.PersistentHashMap α β(σαβm σ) → σm σ
                                                        Equations
                                                        Instances For
                                                          def Lean.PersistentHashMap.forM {m : Type w → Type w'} [Monad m] {α : Type u_1} {β : Type u_2} :
                                                          {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashMap α β(αβm PUnit) → m PUnit
                                                          Equations
                                                          Instances For
                                                            def Lean.PersistentHashMap.foldl {σ : Type w} {α : Type u_1} {β : Type u_2} :
                                                            {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashMap α β(σαβσ) → σσ
                                                            Equations
                                                            Instances For
                                                              def Lean.PersistentHashMap.forIn {m : Type w → Type w'} {σ : Type w} {α : Type u_1} {β : Type u_2} :
                                                              {x : BEq α} → {x_1 : Hashable α} → [inst : Monad m] → Lean.PersistentHashMap α βσ(α × βσm (ForInStep σ)) → m σ
                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              Instances For
                                                                instance Lean.PersistentHashMap.instForInPersistentHashMapProd {m : Type w → Type w'} {α : Type u_1} {β : Type u_2} :
                                                                {x : BEq α} → {x_1 : Hashable α} → ForIn m (Lean.PersistentHashMap α β) (α × β)
                                                                Equations
                                                                • Lean.PersistentHashMap.instForInPersistentHashMapProd = { forIn := fun {β} [Monad m] => Lean.PersistentHashMap.forIn }
                                                                partial def Lean.PersistentHashMap.mapMAux {α : Type u} {β : Type v} {σ : Type u} {m : Type u → Type w} [Monad m] (f : βm σ) (n : Lean.PersistentHashMap.Node α β) :
                                                                def Lean.PersistentHashMap.mapM {α : Type u} {β : Type v} {σ : Type u} {m : Type u → Type w} [Monad m] :
                                                                {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashMap α β(βm σ) → m (Lean.PersistentHashMap α σ)
                                                                Equations
                                                                Instances For
                                                                  def Lean.PersistentHashMap.map {α : Type u} {β : Type v} {σ : Type u} :
                                                                  {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashMap α β(βσ) → Lean.PersistentHashMap α σ
                                                                  Equations
                                                                  Instances For
                                                                    def Lean.PersistentHashMap.toList {α : Type u_1} {β : Type u_2} :
                                                                    {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashMap α βList (α × β)
                                                                    Equations
                                                                    Instances For
                                                                      • numNodes : Nat
                                                                      • numNull : Nat
                                                                      • numCollisions : Nat
                                                                      • maxDepth : Nat
                                                                      Instances For
                                                                        def Lean.PersistentHashMap.stats {α : Type u_1} {β : Type u_2} :
                                                                        {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashMap α βLean.PersistentHashMap.Stats
                                                                        Equations
                                                                        Instances For
                                                                          Equations
                                                                          • One or more equations did not get rendered due to their size.
                                                                          Instances For