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
      @[reducible, inline]
      Equations
      Instances For
        @[reducible, inline]
        Equations
        Instances For
          @[reducible, inline]
          Equations
          Instances For
            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_1 : Hashable α} → Lean.PersistentHashMap α βBool
                    Equations
                    • { root := root }.isEmpty = root.isEmpty
                    Instances For
                      Equations
                      Equations
                      Instances For
                        @[reducible, inline]
                        Equations
                        Instances For
                          @[reducible, inline]
                          Equations
                          Instances For
                            @[reducible, inline]
                            Equations
                            Instances For
                              Instances For
                                @[reducible, inline]
                                abbrev Lean.PersistentHashMap.CollisionNode (α : Type u_1) (β : Type u_2) :
                                Type (max 0 u_2 u_1)
                                Equations
                                Instances For
                                  @[reducible, inline]
                                  abbrev Lean.PersistentHashMap.EntriesNode (α : Type u_1) (β : Type u_2) :
                                  Type (max 0 u_2 u_1)
                                  Equations
                                  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 : keys.size = vals.size) (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 : keys.size = vals.size) (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.instGetElemOptionTrue {α : Type u_1} {β : Type u_2} :
                                          {x : BEq α} → {x_1 : Hashable α} → GetElem (Lean.PersistentHashMap α β) α (Option β) fun (x : Lean.PersistentHashMap α β) (x : α) => True
                                          Equations
                                          • Lean.PersistentHashMap.instGetElemOptionTrue = { getElem := fun (m : Lean.PersistentHashMap α β) (i : α) (x_1 : True) => m.find? i }
                                          @[inline]
                                          def Lean.PersistentHashMap.findD {α : Type u_1} {β : Type u_2} :
                                          {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashMap α βαββ
                                          Equations
                                          • m.findD a b₀ = (m.find? a).getD b₀
                                          Instances For
                                            @[inline]
                                            def Lean.PersistentHashMap.find! {α : Type u_1} {β : Type u_2} :
                                            {x : BEq α} → {x_1 : Hashable α} → [inst : Inhabited β] → Lean.PersistentHashMap α βαβ
                                            Equations
                                            • m.find! a = match m.find? a with | some b => b | none => panicWithPosWithDecl "Lean.Data.PersistentHashMap" "Lean.PersistentHashMap.find!" 170 14 "key is not in the map"
                                            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 α] :
                                              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 : keys.size = vals.size) (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
                                                  Instances For
                                                    partial def Lean.PersistentHashMap.eraseAux {α : Type u_1} {β : Type u_2} [BEq α] :
                                                    def Lean.PersistentHashMap.erase {α : Type u_1} {β : Type u_2} :
                                                    {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashMap α βαLean.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 σ) :
                                                      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 : 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_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
                                                          • map.foldl f init = (map.foldlM f init).run
                                                          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.instForInProd {m : Type w → Type w'} {α : Type u_1} {β : Type u_2} :
                                                              {x : BEq α} → {x_1 : Hashable α} → ForIn m (Lean.PersistentHashMap α β) (α × β)
                                                              Equations
                                                              • Lean.PersistentHashMap.instForInProd = { forIn := fun {β_1 : Type ?u.41} [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
                                                                • pm.map f = (pm.mapM f).run
                                                                Instances For
                                                                  def Lean.PersistentHashMap.toList {α : Type u_1} {β : Type u_2} :
                                                                  {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashMap α βList (α × β)
                                                                  Equations
                                                                  • m.toList = m.foldl (fun (ps : List (α × β)) (k : α) (v : β) => (k, v) :: ps) []
                                                                  Instances For
                                                                    def Lean.PersistentHashMap.toArray {α : Type u_1} {β : Type u_2} :
                                                                    {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashMap α βArray (α × β)
                                                                    Equations
                                                                    • m.toArray = m.foldl (fun (ps : Array (α × β)) (k : α) (v : β) => ps.push (k, v)) #[]
                                                                    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