Documentation

Lean.Data.RBMap

inductive Lean.RBColor :
Instances For
    inductive Lean.RBNode (α : Type u) (β : αType v) :
    Type (max u v)
    Instances For
      def Lean.RBNode.depth {α : Type u} {β : αType v} (f : NatNatNat) :
      Lean.RBNode α βNat
      Equations
      Instances For
        def Lean.RBNode.min {α : Type u} {β : αType v} :
        Lean.RBNode α βOption ((k : α) × β k)
        Equations
        Instances For
          def Lean.RBNode.max {α : Type u} {β : αType v} :
          Lean.RBNode α βOption ((k : α) × β k)
          Equations
          Instances For
            @[specialize #[]]
            def Lean.RBNode.fold {α : Type u} {β : αType v} {σ : Type w} (f : σ(k : α) → β kσ) (init : σ) :
            Lean.RBNode α βσ
            Equations
            Instances For
              @[specialize #[]]
              def Lean.RBNode.forM {α : Type u} {β : αType v} {m : TypeType u_1} [Monad m] (f : (k : α) → β km Unit) :
              Lean.RBNode α βm Unit
              Equations
              Instances For
                @[specialize #[]]
                def Lean.RBNode.foldM {α : Type u} {β : αType v} {σ : Type w} {m : Type w → Type u_1} [Monad m] (f : σ(k : α) → β km σ) (init : σ) :
                Lean.RBNode α βm σ
                Equations
                Instances For
                  @[inline]
                  def Lean.RBNode.forIn {α : Type u} {β : αType v} {σ : Type w} {m : Type w → Type u_1} [Monad m] (as : Lean.RBNode α β) (init : σ) (f : (k : α) → β kσm (ForInStep σ)) :
                  m σ
                  Equations
                  Instances For
                    @[specialize #[]]
                    def Lean.RBNode.forIn.visit {α : Type u} {β : αType v} {σ : Type w} {m : Type w → Type u_1} [Monad m] (f : (k : α) → β kσm (ForInStep σ)) :
                    Lean.RBNode α βσm (ForInStep σ)
                    Equations
                    Instances For
                      @[specialize #[]]
                      def Lean.RBNode.revFold {α : Type u} {β : αType v} {σ : Type w} (f : σ(k : α) → β kσ) (init : σ) :
                      Lean.RBNode α βσ
                      Equations
                      Instances For
                        @[specialize #[]]
                        def Lean.RBNode.all {α : Type u} {β : αType v} (p : (k : α) → β kBool) :
                        Lean.RBNode α βBool
                        Equations
                        Instances For
                          @[specialize #[]]
                          def Lean.RBNode.any {α : Type u} {β : αType v} (p : (k : α) → β kBool) :
                          Lean.RBNode α βBool
                          Equations
                          Instances For
                            def Lean.RBNode.singleton {α : Type u} {β : αType v} (k : α) (v : β k) :
                            Equations
                            Instances For
                              def Lean.RBNode.isSingleton {α : Type u} {β : αType v} :
                              Lean.RBNode α βBool
                              Equations
                              Instances For
                                @[inline]
                                def Lean.RBNode.balance1 {α : Type u} {β : αType v} :
                                Lean.RBNode α β(a : α) → β aLean.RBNode α βLean.RBNode α β
                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  @[inline]
                                  def Lean.RBNode.balance2 {α : Type u} {β : αType v} :
                                  Lean.RBNode α β(a : α) → β aLean.RBNode α βLean.RBNode α β
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    def Lean.RBNode.isRed {α : Type u} {β : αType v} :
                                    Lean.RBNode α βBool
                                    Equations
                                    Instances For
                                      def Lean.RBNode.isBlack {α : Type u} {β : αType v} :
                                      Lean.RBNode α βBool
                                      Equations
                                      Instances For
                                        @[specialize #[]]
                                        def Lean.RBNode.ins {α : Type u} {β : αType v} (cmp : ααOrdering) :
                                        Lean.RBNode α β(k : α) → β kLean.RBNode α β
                                        Equations
                                        Instances For
                                          def Lean.RBNode.setBlack {α : Type u} {β : αType v} :
                                          Lean.RBNode α βLean.RBNode α β
                                          Equations
                                          Instances For
                                            @[specialize #[]]
                                            def Lean.RBNode.insert {α : Type u} {β : αType v} (cmp : ααOrdering) (t : Lean.RBNode α β) (k : α) (v : β k) :
                                            Equations
                                            Instances For
                                              def Lean.RBNode.setRed {α : Type u} {β : αType v} :
                                              Lean.RBNode α βLean.RBNode α β
                                              Equations
                                              Instances For
                                                def Lean.RBNode.balLeft {α : Type u} {β : αType v} :
                                                Lean.RBNode α β(k : α) → β kLean.RBNode α βLean.RBNode α β
                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  def Lean.RBNode.balRight {α : Type u} {β : αType v} (l : Lean.RBNode α β) (k : α) (v : β k) (r : Lean.RBNode α β) :
                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    def Lean.RBNode.size {α : Type u} {β : αType v} :
                                                    Lean.RBNode α βNat

                                                    The number of nodes in the tree.

                                                    Equations
                                                    Instances For
                                                      @[irreducible]
                                                      def Lean.RBNode.appendTrees {α : Type u} {β : αType v} :
                                                      Lean.RBNode α βLean.RBNode α βLean.RBNode α β
                                                      Equations
                                                      Instances For
                                                        @[specialize #[]]
                                                        def Lean.RBNode.del {α : Type u} {β : αType v} (cmp : ααOrdering) (x : α) :
                                                        Lean.RBNode α βLean.RBNode α β
                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        • Lean.RBNode.del cmp x Lean.RBNode.leaf = Lean.RBNode.leaf
                                                        Instances For
                                                          @[specialize #[]]
                                                          def Lean.RBNode.erase {α : Type u} {β : αType v} (cmp : ααOrdering) (x : α) (t : Lean.RBNode α β) :
                                                          Equations
                                                          Instances For
                                                            @[specialize #[]]
                                                            def Lean.RBNode.findCore {α : Type u} {β : αType v} (cmp : ααOrdering) :
                                                            Lean.RBNode α βαOption ((k : α) × β k)
                                                            Equations
                                                            • One or more equations did not get rendered due to their size.
                                                            • Lean.RBNode.findCore cmp Lean.RBNode.leaf x = none
                                                            Instances For
                                                              @[specialize #[]]
                                                              def Lean.RBNode.find {α : Type u} (cmp : ααOrdering) {β : Type v} :
                                                              (Lean.RBNode α fun (x : α) => β)αOption β
                                                              Equations
                                                              Instances For
                                                                @[specialize #[]]
                                                                def Lean.RBNode.lowerBound {α : Type u} {β : αType v} (cmp : ααOrdering) :
                                                                Lean.RBNode α βαOption (Sigma β)Option (Sigma β)
                                                                Equations
                                                                • One or more equations did not get rendered due to their size.
                                                                • Lean.RBNode.lowerBound cmp Lean.RBNode.leaf x✝ x = x
                                                                Instances For
                                                                  inductive Lean.RBNode.WellFormed {α : Type u} {β : αType v} (cmp : ααOrdering) :
                                                                  Lean.RBNode α βProp
                                                                  Instances For
                                                                    @[specialize #[]]
                                                                    def Lean.RBNode.mapM {α : Type v} {β : αType v} {γ : αType v} {M : Type v → Type v} [Applicative M] (f : (a : α) → β aM (γ a)) :
                                                                    Lean.RBNode α βM (Lean.RBNode α γ)
                                                                    Equations
                                                                    • One or more equations did not get rendered due to their size.
                                                                    • Lean.RBNode.mapM f Lean.RBNode.leaf = pure Lean.RBNode.leaf
                                                                    Instances For
                                                                      @[specialize #[]]
                                                                      def Lean.RBNode.map {α : Type u} {β : αType v} {γ : αType v} (f : (a : α) → β aγ a) :
                                                                      Lean.RBNode α βLean.RBNode α γ
                                                                      Equations
                                                                      Instances For
                                                                        def Lean.RBNode.toArray {α : Type u} {β : αType v} (n : Lean.RBNode α β) :
                                                                        Equations
                                                                        Instances For
                                                                          instance Lean.RBNode.instEmptyCollection {α : Type u} {β : αType v} :
                                                                          Equations
                                                                          • Lean.RBNode.instEmptyCollection = { emptyCollection := Lean.RBNode.leaf }
                                                                          def Lean.RBMap (α : Type u) (β : Type v) (cmp : ααOrdering) :
                                                                          Type (max u v)
                                                                          Equations
                                                                          Instances For
                                                                            @[inline]
                                                                            def Lean.mkRBMap (α : Type u) (β : Type v) (cmp : ααOrdering) :
                                                                            Lean.RBMap α β cmp
                                                                            Equations
                                                                            Instances For
                                                                              @[inline]
                                                                              def Lean.RBMap.empty {α : Type u} {β : Type v} {cmp : ααOrdering} :
                                                                              Lean.RBMap α β cmp
                                                                              Equations
                                                                              Instances For
                                                                                instance Lean.instEmptyCollectionRBMap (α : Type u) (β : Type v) (cmp : ααOrdering) :
                                                                                Equations
                                                                                instance Lean.instInhabitedRBMap (α : Type u) (β : Type v) (cmp : ααOrdering) :
                                                                                Inhabited (Lean.RBMap α β cmp)
                                                                                Equations
                                                                                def Lean.RBMap.depth {α : Type u} {β : Type v} {cmp : ααOrdering} (f : NatNatNat) (t : Lean.RBMap α β cmp) :
                                                                                Equations
                                                                                Instances For
                                                                                  def Lean.RBMap.isSingleton {α : Type u} {β : Type v} {cmp : ααOrdering} (t : Lean.RBMap α β cmp) :
                                                                                  Equations
                                                                                  • t.isSingleton = t.val.isSingleton
                                                                                  Instances For
                                                                                    @[inline]
                                                                                    def Lean.RBMap.fold {α : Type u} {β : Type v} {σ : Type w} {cmp : ααOrdering} (f : σαβσ) (init : σ) :
                                                                                    Lean.RBMap α β cmpσ
                                                                                    Equations
                                                                                    Instances For
                                                                                      @[inline]
                                                                                      def Lean.RBMap.revFold {α : Type u} {β : Type v} {σ : Type w} {cmp : ααOrdering} (f : σαβσ) (init : σ) :
                                                                                      Lean.RBMap α β cmpσ
                                                                                      Equations
                                                                                      Instances For
                                                                                        @[inline]
                                                                                        def Lean.RBMap.foldM {α : Type u} {β : Type v} {σ : Type w} {cmp : ααOrdering} {m : Type w → Type u_1} [Monad m] (f : σαβm σ) (init : σ) :
                                                                                        Lean.RBMap α β cmpm σ
                                                                                        Equations
                                                                                        Instances For
                                                                                          @[inline]
                                                                                          def Lean.RBMap.forM {α : Type u} {β : Type v} {cmp : ααOrdering} {m : Type u_1 → Type u_2} [Monad m] (f : αβm PUnit) (t : Lean.RBMap α β cmp) :
                                                                                          Equations
                                                                                          Instances For
                                                                                            @[inline]
                                                                                            def Lean.RBMap.forIn {α : Type u} {β : Type v} {σ : Type w} {cmp : ααOrdering} {m : Type w → Type u_1} [Monad m] (t : Lean.RBMap α β cmp) (init : σ) (f : α × βσm (ForInStep σ)) :
                                                                                            m σ
                                                                                            Equations
                                                                                            • t.forIn init f = t.val.forIn init fun (a : α) (b : β) (acc : σ) => f (a, b) acc
                                                                                            Instances For
                                                                                              instance Lean.RBMap.instForInProd {α : Type u} {β : Type v} {cmp : ααOrdering} {m : Type u_1 → Type u_2} :
                                                                                              ForIn m (Lean.RBMap α β cmp) (α × β)
                                                                                              Equations
                                                                                              • Lean.RBMap.instForInProd = { forIn := fun {β_1 : Type u_1} [Monad m] => Lean.RBMap.forIn }
                                                                                              @[inline]
                                                                                              def Lean.RBMap.isEmpty {α : Type u} {β : Type v} {cmp : ααOrdering} :
                                                                                              Lean.RBMap α β cmpBool
                                                                                              Equations
                                                                                              • x.isEmpty = match x with | Lean.RBNode.leaf, property => true | x => false
                                                                                              Instances For
                                                                                                @[specialize #[]]
                                                                                                def Lean.RBMap.toList {α : Type u} {β : Type v} {cmp : ααOrdering} :
                                                                                                Lean.RBMap α β cmpList (α × β)
                                                                                                Equations
                                                                                                Instances For
                                                                                                  @[inline]
                                                                                                  def Lean.RBMap.min {α : Type u} {β : Type v} {cmp : ααOrdering} :
                                                                                                  Lean.RBMap α β cmpOption (α × β)

                                                                                                  Returns the kv pair (a,b) such that a ≤ k for all keys in the RBMap.

                                                                                                  Equations
                                                                                                  • x.min = match x with | t, property => match t.min with | some k, v => some (k, v) | none => none
                                                                                                  Instances For
                                                                                                    @[inline]
                                                                                                    def Lean.RBMap.max {α : Type u} {β : Type v} {cmp : ααOrdering} :
                                                                                                    Lean.RBMap α β cmpOption (α × β)

                                                                                                    Returns the kv pair (a,b) such that a ≥ k for all keys in the RBMap.

                                                                                                    Equations
                                                                                                    • x.max = match x with | t, property => match t.max with | some k, v => some (k, v) | none => none
                                                                                                    Instances For
                                                                                                      instance Lean.RBMap.instRepr {α : Type u} {β : Type v} {cmp : ααOrdering} [Repr α] [Repr β] :
                                                                                                      Repr (Lean.RBMap α β cmp)
                                                                                                      Equations
                                                                                                      @[inline]
                                                                                                      def Lean.RBMap.insert {α : Type u} {β : Type v} {cmp : ααOrdering} :
                                                                                                      Lean.RBMap α β cmpαβLean.RBMap α β cmp
                                                                                                      Equations
                                                                                                      • x✝¹.insert x✝ x = match x✝¹, x✝, x with | t, w, k, v => Lean.RBNode.insert cmp t k v,
                                                                                                      Instances For
                                                                                                        @[inline]
                                                                                                        def Lean.RBMap.erase {α : Type u} {β : Type v} {cmp : ααOrdering} :
                                                                                                        Lean.RBMap α β cmpαLean.RBMap α β cmp
                                                                                                        Equations
                                                                                                        Instances For
                                                                                                          @[specialize #[]]
                                                                                                          def Lean.RBMap.ofList {α : Type u} {β : Type v} {cmp : ααOrdering} :
                                                                                                          List (α × β)Lean.RBMap α β cmp
                                                                                                          Equations
                                                                                                          Instances For
                                                                                                            @[inline]
                                                                                                            def Lean.RBMap.findCore? {α : Type u} {β : Type v} {cmp : ααOrdering} :
                                                                                                            Lean.RBMap α β cmpαOption ((_ : α) × β)
                                                                                                            Equations
                                                                                                            Instances For
                                                                                                              @[inline]
                                                                                                              def Lean.RBMap.find? {α : Type u} {β : Type v} {cmp : ααOrdering} :
                                                                                                              Lean.RBMap α β cmpαOption β
                                                                                                              Equations
                                                                                                              Instances For
                                                                                                                @[inline]
                                                                                                                def Lean.RBMap.findD {α : Type u} {β : Type v} {cmp : ααOrdering} (t : Lean.RBMap α β cmp) (k : α) (v₀ : β) :
                                                                                                                β
                                                                                                                Equations
                                                                                                                • t.findD k v₀ = (t.find? k).getD v₀
                                                                                                                Instances For
                                                                                                                  @[inline]
                                                                                                                  def Lean.RBMap.lowerBound {α : Type u} {β : Type v} {cmp : ααOrdering} :
                                                                                                                  Lean.RBMap α β cmpαOption ((_ : α) × β)

                                                                                                                  (lowerBound k) retrieves the kv pair of the largest key smaller than or equal to k, if it exists.

                                                                                                                  Equations
                                                                                                                  Instances For
                                                                                                                    @[inline]
                                                                                                                    def Lean.RBMap.contains {α : Type u} {β : Type v} {cmp : ααOrdering} (t : Lean.RBMap α β cmp) (a : α) :

                                                                                                                    Returns true if the given key a is in the RBMap.

                                                                                                                    Equations
                                                                                                                    • t.contains a = (t.find? a).isSome
                                                                                                                    Instances For
                                                                                                                      @[inline]
                                                                                                                      def Lean.RBMap.fromList {α : Type u} {β : Type v} (l : List (α × β)) (cmp : ααOrdering) :
                                                                                                                      Lean.RBMap α β cmp
                                                                                                                      Equations
                                                                                                                      Instances For
                                                                                                                        @[inline]
                                                                                                                        def Lean.RBMap.fromArray {α : Type u} {β : Type v} (l : Array (α × β)) (cmp : ααOrdering) :
                                                                                                                        Lean.RBMap α β cmp
                                                                                                                        Equations
                                                                                                                        Instances For
                                                                                                                          @[inline]
                                                                                                                          def Lean.RBMap.all {α : Type u} {β : Type v} {cmp : ααOrdering} :
                                                                                                                          Lean.RBMap α β cmp(αβBool)Bool

                                                                                                                          Returns true if the given predicate is true for all items in the RBMap.

                                                                                                                          Equations
                                                                                                                          Instances For
                                                                                                                            @[inline]
                                                                                                                            def Lean.RBMap.any {α : Type u} {β : Type v} {cmp : ααOrdering} :
                                                                                                                            Lean.RBMap α β cmp(αβBool)Bool

                                                                                                                            Returns true if the given predicate is true for any item in the RBMap.

                                                                                                                            Equations
                                                                                                                            Instances For
                                                                                                                              def Lean.RBMap.size {α : Type u} {β : Type v} {cmp : ααOrdering} (m : Lean.RBMap α β cmp) :

                                                                                                                              The number of items in the RBMap.

                                                                                                                              Equations
                                                                                                                              Instances For
                                                                                                                                def Lean.RBMap.maxDepth {α : Type u} {β : Type v} {cmp : ααOrdering} (t : Lean.RBMap α β cmp) :
                                                                                                                                Equations
                                                                                                                                Instances For
                                                                                                                                  @[inline]
                                                                                                                                  def Lean.RBMap.min! {α : Type u} {β : Type v} {cmp : ααOrdering} [Inhabited α] [Inhabited β] (t : Lean.RBMap α β cmp) :
                                                                                                                                  α × β
                                                                                                                                  Equations
                                                                                                                                  • t.min! = match t.min with | some p => p | none => panicWithPosWithDecl "Lean.Data.RBMap" "Lean.RBMap.min!" 373 14 "map is empty"
                                                                                                                                  Instances For
                                                                                                                                    @[inline]
                                                                                                                                    def Lean.RBMap.max! {α : Type u} {β : Type v} {cmp : ααOrdering} [Inhabited α] [Inhabited β] (t : Lean.RBMap α β cmp) :
                                                                                                                                    α × β
                                                                                                                                    Equations
                                                                                                                                    • t.max! = match t.max with | some p => p | none => panicWithPosWithDecl "Lean.Data.RBMap" "Lean.RBMap.max!" 378 14 "map is empty"
                                                                                                                                    Instances For
                                                                                                                                      @[inline]
                                                                                                                                      def Lean.RBMap.find! {α : Type u} {β : Type v} {cmp : ααOrdering} [Inhabited β] (t : Lean.RBMap α β cmp) (k : α) :
                                                                                                                                      β

                                                                                                                                      Attempts to find the value with key k : α in t and panics if there is no such key.

                                                                                                                                      Equations
                                                                                                                                      • t.find! k = match t.find? k with | some b => b | none => panicWithPosWithDecl "Lean.Data.RBMap" "Lean.RBMap.find!" 384 14 "key is not in the map"
                                                                                                                                      Instances For
                                                                                                                                        def Lean.RBMap.mergeBy {α : Type u} {β : Type v} {cmp : ααOrdering} (mergeFn : αβββ) (t₁ : Lean.RBMap α β cmp) (t₂ : Lean.RBMap α β cmp) :
                                                                                                                                        Lean.RBMap α β cmp

                                                                                                                                        Merges the maps t₁ and t₂, if a key a : α exists in both, then use mergeFn a b₁ b₂ to produce the new merged value.

                                                                                                                                        Equations
                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                        Instances For
                                                                                                                                          def Lean.RBMap.intersectBy {α : Type u} {β : Type v} {cmp : ααOrdering} {γ : Type v₁} {δ : Type v₂} (mergeFn : αβγδ) (t₁ : Lean.RBMap α β cmp) (t₂ : Lean.RBMap α γ cmp) :
                                                                                                                                          Lean.RBMap α δ cmp

                                                                                                                                          Intersects the maps t₁ and t₂ using mergeFn a b₁ b₂ to produce the new value.

                                                                                                                                          Equations
                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                          Instances For
                                                                                                                                            def Lean.rbmapOf {α : Type u} {β : Type v} (l : List (α × β)) (cmp : ααOrdering) :
                                                                                                                                            Lean.RBMap α β cmp
                                                                                                                                            Equations
                                                                                                                                            Instances For