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 σ
                  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) :
                            Instances For
                              @[inline]
                              def Lean.RBNode.balance1 {α : Type u} {β : αType v} :
                              Lean.RBNode α β(a : α) → β aLean.RBNode α βLean.RBNode α β
                              Instances For
                                @[inline]
                                def Lean.RBNode.balance2 {α : Type u} {β : αType v} :
                                Lean.RBNode α β(a : α) → β aLean.RBNode α βLean.RBNode α β
                                Instances For
                                  def Lean.RBNode.isRed {α : Type u} {β : αType v} :
                                  Lean.RBNode α βBool
                                  Instances For
                                    def Lean.RBNode.isBlack {α : Type u} {β : αType v} :
                                    Lean.RBNode α βBool
                                    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 α β
                                        Instances For
                                          @[specialize #[]]
                                          def Lean.RBNode.insert {α : Type u} {β : αType v} (cmp : ααOrdering) (t : Lean.RBNode α β) (k : α) (v : β k) :
                                          Instances For
                                            def Lean.RBNode.setRed {α : Type u} {β : αType v} :
                                            Lean.RBNode α βLean.RBNode α β
                                            Instances For
                                              def Lean.RBNode.balLeft {α : Type u} {β : αType v} :
                                              Lean.RBNode α β(k : α) → β kLean.RBNode α βLean.RBNode α β
                                              Instances For
                                                def Lean.RBNode.balRight {α : Type u} {β : αType v} (l : Lean.RBNode α β) (k : α) (v : β k) (r : Lean.RBNode α β) :
                                                Instances For
                                                  def Lean.RBNode.size {α : Type u} {β : αType v} :
                                                  Lean.RBNode α βNat

                                                  The number of nodes in the tree.

                                                  Equations
                                                  Instances For
                                                    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 α β) :
                                                        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
                                                            • One or more equations did not get rendered due to their size.
                                                            • Lean.RBNode.find cmp Lean.RBNode.leaf x = none
                                                            Instances For
                                                              @[specialize #[]]
                                                              def Lean.RBNode.lowerBound {α : Type u} {β : αType v} (cmp : ααOrdering) :
                                                              Lean.RBNode α βαOption (Sigma β)Option (Sigma β)
                                                              Equations
                                                              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 α β) :
                                                                      Instances For
                                                                        def Lean.RBMap (α : Type u) (β : Type v) (cmp : ααOrdering) :
                                                                        Type (max u v)
                                                                        Instances For
                                                                          @[inline]
                                                                          def Lean.mkRBMap (α : Type u) (β : Type v) (cmp : ααOrdering) :
                                                                          Lean.RBMap α β cmp
                                                                          Instances For
                                                                            @[inline]
                                                                            def Lean.RBMap.empty {α : Type u} {β : Type v} {cmp : ααOrdering} :
                                                                            Lean.RBMap α β cmp
                                                                            Instances For
                                                                              instance Lean.instEmptyCollectionRBMap (α : Type u) (β : Type v) (cmp : ααOrdering) :
                                                                              instance Lean.instInhabitedRBMap (α : Type u) (β : Type v) (cmp : ααOrdering) :
                                                                              Inhabited (Lean.RBMap α β cmp)
                                                                              def Lean.RBMap.depth {α : Type u} {β : Type v} {cmp : ααOrdering} (f : NatNatNat) (t : Lean.RBMap α β cmp) :
                                                                              Instances For
                                                                                @[inline]
                                                                                def Lean.RBMap.fold {α : Type u} {β : Type v} {σ : Type w} {cmp : ααOrdering} (f : σαβσ) (init : σ) :
                                                                                Lean.RBMap α β cmpσ
                                                                                Instances For
                                                                                  @[inline]
                                                                                  def Lean.RBMap.revFold {α : Type u} {β : Type v} {σ : Type w} {cmp : ααOrdering} (f : σαβσ) (init : σ) :
                                                                                  Lean.RBMap α β cmpσ
                                                                                  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 σ
                                                                                    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) :
                                                                                      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 σ
                                                                                        Instances For
                                                                                          instance Lean.RBMap.instForInRBMapProd {α : Type u} {β : Type v} {cmp : ααOrdering} {m : Type u_1 → Type u_2} :
                                                                                          ForIn m (Lean.RBMap α β cmp) (α × β)
                                                                                          @[inline]
                                                                                          def Lean.RBMap.isEmpty {α : Type u} {β : Type v} {cmp : ααOrdering} :
                                                                                          Lean.RBMap α β cmpBool
                                                                                          Instances For
                                                                                            @[specialize #[]]
                                                                                            def Lean.RBMap.toList {α : Type u} {β : Type v} {cmp : ααOrdering} :
                                                                                            Lean.RBMap α β cmpList (α × β)
                                                                                            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.

                                                                                              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.

                                                                                                Instances For
                                                                                                  instance Lean.RBMap.instReprRBMap {α : Type u} {β : Type v} {cmp : ααOrdering} [Repr α] [Repr β] :
                                                                                                  Repr (Lean.RBMap α β cmp)
                                                                                                  @[inline]
                                                                                                  def Lean.RBMap.insert {α : Type u} {β : Type v} {cmp : ααOrdering} :
                                                                                                  Lean.RBMap α β cmpαβLean.RBMap α β cmp
                                                                                                  Instances For
                                                                                                    @[inline]
                                                                                                    def Lean.RBMap.erase {α : Type u} {β : Type v} {cmp : ααOrdering} :
                                                                                                    Lean.RBMap α β cmpαLean.RBMap α β cmp
                                                                                                    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 ((_ : α) × β)
                                                                                                        Instances For
                                                                                                          @[inline]
                                                                                                          def Lean.RBMap.find? {α : Type u} {β : Type v} {cmp : ααOrdering} :
                                                                                                          Lean.RBMap α β cmpαOption β
                                                                                                          Instances For
                                                                                                            @[inline]
                                                                                                            def Lean.RBMap.findD {α : Type u} {β : Type v} {cmp : ααOrdering} (t : Lean.RBMap α β cmp) (k : α) (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.

                                                                                                              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.

                                                                                                                Instances For
                                                                                                                  @[inline]
                                                                                                                  def Lean.RBMap.fromList {α : Type u} {β : Type v} (l : List (α × β)) (cmp : ααOrdering) :
                                                                                                                  Lean.RBMap α β cmp
                                                                                                                  Instances For
                                                                                                                    @[inline]
                                                                                                                    def Lean.RBMap.fromArray {α : Type u} {β : Type v} (l : Array (α × β)) (cmp : ααOrdering) :
                                                                                                                    Lean.RBMap α β cmp
                                                                                                                    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.

                                                                                                                      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.

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

                                                                                                                          The number of items in the RBMap.

                                                                                                                          Instances For
                                                                                                                            def Lean.RBMap.maxDepth {α : Type u} {β : Type v} {cmp : ααOrdering} (t : Lean.RBMap α β cmp) :
                                                                                                                            Instances For
                                                                                                                              @[inline]
                                                                                                                              def Lean.RBMap.min! {α : Type u} {β : Type v} {cmp : ααOrdering} [Inhabited α] [Inhabited β] (t : Lean.RBMap α β cmp) :
                                                                                                                              α × β
                                                                                                                              Instances For
                                                                                                                                @[inline]
                                                                                                                                def Lean.RBMap.max! {α : Type u} {β : Type v} {cmp : ααOrdering} [Inhabited α] [Inhabited β] (t : Lean.RBMap α β cmp) :
                                                                                                                                α × β
                                                                                                                                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.

                                                                                                                                  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.

                                                                                                                                    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.

                                                                                                                                      Instances For
                                                                                                                                        def Lean.rbmapOf {α : Type u} {β : Type v} (l : List (α × β)) (cmp : ααOrdering) :
                                                                                                                                        Lean.RBMap α β cmp
                                                                                                                                        Instances For