Documentation

Batteries.Data.RBMap.Basic

Red-black trees #

This module implements a type RBMap α β cmp which is a functional data structure for storing a key-value store in a binary search tree.

It is built on the simpler RBSet α cmp type, which stores a set of values of type α using the function cmp : α → α → Ordering for determining the ordering relation. The tree will never store two elements that compare .eq under the cmp function, but the function does not have to satisfy cmp x y = .eq → x = y, and in the map case α is a key-value pair and the cmp function only compares the keys.

In a red-black tree, every node has a color which is either "red" or "black" (this particular choice of colors is conventional). A nil node is considered black.

  • red: Batteries.RBColor

    A red node is required to have black children.

  • black: Batteries.RBColor

    Every path from the root to a leaf must pass through the same number of black nodes.

Instances For
    inductive Batteries.RBNode (α : Type u) :

    A red-black tree. (This is an internal implementation detail of the RBSet type, which includes the invariants of the tree.) This is a binary search tree augmented with a "color" field which is either red or black for each node and used to implement the re-balancing operations. See: Red–black tree

    Instances For
      instance Batteries.instReprRBNode :
      {α : Type u_1} → [inst : Repr α] → Repr (Batteries.RBNode α)
      Equations
      • Batteries.instReprRBNode = { reprPrec := Batteries.reprRBNode✝ }
      Equations
      • Batteries.RBNode.instEmptyCollection = { emptyCollection := Batteries.RBNode.nil }

      The minimum element of a tree is the left-most value.

      Equations
      Instances For

        The maximum element of a tree is the right-most value.

        Equations
        Instances For
          @[deprecated Batteries.RBNode.min?]

          Alias of Batteries.RBNode.min?.


          The minimum element of a tree is the left-most value.

          Equations
          Instances For
            @[deprecated Batteries.RBNode.max?]

            Alias of Batteries.RBNode.max?.


            The maximum element of a tree is the right-most value.

            Equations
            Instances For
              @[specialize #[]]
              def Batteries.RBNode.fold {σ : Sort u_1} {α : Type u_2} (v₀ : σ) (f : σασσ) :

              Fold a function in tree order along the nodes. v₀ is used at nil nodes and f is used to combine results at branching nodes.

              Equations
              Instances For
                @[specialize #[]]
                def Batteries.RBNode.foldl {σ : Sort u_1} {α : Type u_2} (f : σασ) (init : σ) :

                Fold a function on the values from left to right (in increasing order).

                Equations
                Instances For
                  @[specialize #[]]
                  def Batteries.RBNode.foldr {α : Type u_1} {σ : Sort u_2} (f : ασσ) :
                  Batteries.RBNode ασσ

                  Fold a function on the values from right to left (in decreasing order).

                  Equations
                  Instances For

                    O(n). Convert the tree to a list in ascending order.

                    Equations
                    Instances For
                      @[specialize #[]]
                      def Batteries.RBNode.forM {m : Type u_1 → Type u_2} {α : Type u_3} [Monad m] (f : αm PUnit) :

                      Run monadic function f on each element of the tree (in increasing order).

                      Equations
                      Instances For
                        @[specialize #[]]
                        def Batteries.RBNode.foldlM {m : Type u_1 → Type u_2} {σ : Type u_1} {α : Type u_3} [Monad m] (f : σαm σ) (init : σ) :
                        Batteries.RBNode αm σ

                        Fold a monadic function on the values from left to right (in increasing order).

                        Equations
                        Instances For
                          @[inline]
                          def Batteries.RBNode.forIn {m : Type u_1 → Type u_2} {α : Type u_3} {σ : Type u_1} [Monad m] (as : Batteries.RBNode α) (init : σ) (f : ασm (ForInStep σ)) :
                          m σ

                          Implementation of for x in t loops over a RBNode (in increasing order).

                          Equations
                          Instances For
                            @[specialize #[]]
                            def Batteries.RBNode.forIn.visit {m : Type u_1 → Type u_2} {α : Type u_3} {σ : Type u_1} [Monad m] (f : ασm (ForInStep σ)) :
                            Batteries.RBNode ασm (ForInStep σ)

                            Inner loop of forIn.

                            Equations
                            Instances For
                              instance Batteries.RBNode.instForIn {m : Type u_1 → Type u_2} {α : Type u_3} :
                              Equations
                              • Batteries.RBNode.instForIn = { forIn := fun {β : Type ?u.21} [Monad m] => Batteries.RBNode.forIn }
                              inductive Batteries.RBNode.Stream (α : Type u_1) :
                              Type u_1

                              An auxiliary data structure (an iterator) over an RBNode which lazily pulls elements from the left.

                              Instances For
                                def Batteries.RBNode.toStream {α : Type u_1} :
                                Batteries.RBNode αoptParam (Batteries.RBNode.Stream α) Batteries.RBNode.Stream.nilBatteries.RBNode.Stream α

                                O(log n). Turn a node into a stream, by descending along the left spine.

                                Equations
                                Instances For

                                  O(1) amortized, O(log n) worst case: Get the next element from the stream.

                                  Equations
                                  Instances For
                                    @[specialize #[]]
                                    def Batteries.RBNode.Stream.foldl {σ : Sort u_1} {α : Type u_2} (f : σασ) (init : σ) :

                                    Fold a function on the values from left to right (in increasing order).

                                    Equations
                                    Instances For
                                      @[specialize #[]]
                                      def Batteries.RBNode.Stream.foldr {α : Type u_1} {σ : Sort u_2} (f : ασσ) :
                                      Batteries.RBNode.Stream ασσ

                                      Fold a function on the values from right to left (in decreasing order).

                                      Equations
                                      Instances For

                                        O(n). Convert the stream to a list in ascending order.

                                        Equations
                                        Instances For
                                          Equations
                                          • Batteries.RBNode.instToStreamStream = { toStream := fun (x : Batteries.RBNode α) => x.toStream }
                                          Equations
                                          • Batteries.RBNode.instStreamStream = { next? := Batteries.RBNode.Stream.next? }
                                          @[specialize #[]]
                                          def Batteries.RBNode.all {α : Type u_1} (p : αBool) :

                                          Returns true iff every element of the tree satisfies p.

                                          Equations
                                          Instances For
                                            @[specialize #[]]
                                            def Batteries.RBNode.any {α : Type u_1} (p : αBool) :

                                            Returns true iff any element of the tree satisfies p.

                                            Equations
                                            Instances For
                                              def Batteries.RBNode.All {α : Type u_1} (p : αProp) :

                                              Asserts that p holds on every element of the tree.

                                              Equations
                                              Instances For
                                                theorem Batteries.RBNode.All.imp {α : Type u_1} {p : αProp} {q : αProp} (H : ∀ {x : α}, p xq x) {t : Batteries.RBNode α} :
                                                theorem Batteries.RBNode.all_iff {α : Type u_1} {p : αBool} {t : Batteries.RBNode α} :
                                                Equations
                                                def Batteries.RBNode.Any {α : Type u_1} (p : αProp) :

                                                Asserts that p holds on some element of the tree.

                                                Equations
                                                Instances For
                                                  theorem Batteries.RBNode.any_iff {α : Type u_1} {p : αBool} {t : Batteries.RBNode α} :
                                                  Equations
                                                  def Batteries.RBNode.EMem {α : Type u_1} (x : α) (t : Batteries.RBNode α) :

                                                  True if x is an element of t "exactly", i.e. up to equality, not the cmp relation.

                                                  Equations
                                                  Instances For
                                                    Equations
                                                    def Batteries.RBNode.MemP {α : Type u_1} (cut : αOrdering) (t : Batteries.RBNode α) :

                                                    True if the specified cut matches at least one element of of t.

                                                    Equations
                                                    Instances For
                                                      @[reducible]
                                                      def Batteries.RBNode.Mem {α : Type u_1} (cmp : ααOrdering) (x : α) (t : Batteries.RBNode α) :

                                                      True if x is equivalent to an element of t.

                                                      Equations
                                                      Instances For
                                                        Equations
                                                        Instances For
                                                          Equations
                                                          Instances For
                                                            def Batteries.RBNode.Slow.instDecidableMem {α : Type u_1} {cmp : ααOrdering} {x : α} {t : Batteries.RBNode α} :
                                                            Equations
                                                            Instances For
                                                              @[specialize #[]]
                                                              def Batteries.RBNode.all₂ {α : Type u_1} {β : Type u_2} (R : αβBool) (t₁ : Batteries.RBNode α) (t₂ : Batteries.RBNode β) :

                                                              Asserts that t₁ and t₂ have the same number of elements in the same order, and R holds pairwise between them. The tree structure is ignored.

                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              Instances For
                                                                instance Batteries.RBNode.instBEq {α : Type u_1} [BEq α] :
                                                                Equations
                                                                def Batteries.RBNode.cmpLT {α : Sort u_1} (cmp : ααOrdering) (x : α) (y : α) :

                                                                We say that x < y under the comparator cmp if cmp x y = .lt.

                                                                • In order to avoid assuming the comparator is always lawful, we use a local ∀ [TransCmp cmp] binder in the relation so that the ordering properties of the tree only need to hold if the comparator is lawful.
                                                                • The Nonempty wrapper is a no-op because this is already a proposition, but it prevents the [TransCmp cmp] binder from being introduced when we don't want it.
                                                                Equations
                                                                Instances For
                                                                  theorem Batteries.RBNode.cmpLT_iff :
                                                                  ∀ {α : Sort u_1} {cmp : ααOrdering} {x y : α} [inst : Batteries.TransCmp cmp], Batteries.RBNode.cmpLT cmp x y cmp x y = Ordering.lt
                                                                  instance Batteries.RBNode.instDecidableCmpLTOfTransCmp :
                                                                  {α : Sort u_1} → {x y : α} → (cmp : ααOrdering) → [inst : Batteries.TransCmp cmp] → Decidable (Batteries.RBNode.cmpLT cmp x y)
                                                                  Equations
                                                                  def Batteries.RBNode.cmpEq {α : Sort u_1} (cmp : ααOrdering) (x : α) (y : α) :

                                                                  We say that x ≈ y under the comparator cmp if cmp x y = .eq. See also cmpLT.

                                                                  Equations
                                                                  Instances For
                                                                    theorem Batteries.RBNode.cmpEq_iff :
                                                                    ∀ {α : Sort u_1} {cmp : ααOrdering} {x y : α} [inst : Batteries.TransCmp cmp], Batteries.RBNode.cmpEq cmp x y cmp x y = Ordering.eq
                                                                    instance Batteries.RBNode.instDecidableCmpEqOfTransCmp :
                                                                    {α : Sort u_1} → {x y : α} → (cmp : ααOrdering) → [inst : Batteries.TransCmp cmp] → Decidable (Batteries.RBNode.cmpEq cmp x y)
                                                                    Equations
                                                                    def Batteries.RBNode.isOrdered {α : Type u_1} (cmp : ααOrdering) (t : Batteries.RBNode α) (l : optParam (Option α) none) (r : optParam (Option α) none) :

                                                                    O(n). Verifies an ordering relation on the nodes of the tree.

                                                                    Equations
                                                                    Instances For
                                                                      @[inline]

                                                                      The first half of Okasaki's balance, concerning red-red sequences in the left child.

                                                                      Equations
                                                                      Instances For
                                                                        @[inline]

                                                                        The second half of Okasaki's balance, concerning red-red sequences in the right child.

                                                                        Equations
                                                                        Instances For
                                                                          @[inline]

                                                                          Returns red if the node is red, otherwise black. (Nil nodes are treated as black.)

                                                                          Equations
                                                                          Instances For
                                                                            @[inline]

                                                                            Returns black if the node is black, otherwise red. (Nil nodes are treated as red, which is not the usual convention but useful for deletion.)

                                                                            Equations
                                                                            Instances For

                                                                              Changes the color of the root to black.

                                                                              Equations
                                                                              Instances For

                                                                                O(n). Reverses the ordering of the tree without any rebalancing.

                                                                                Equations
                                                                                Instances For
                                                                                  @[specialize #[]]
                                                                                  def Batteries.RBNode.ins {α : Type u_1} (cmp : ααOrdering) (x : α) :

                                                                                  The core of the insert function. This adds an element x to a balanced red-black tree. Importantly, the result of calling ins is not a proper red-black tree, because it has a broken balance invariant. (See Balanced.ins for the balance invariant of ins.) The insert function does the final fixup needed to restore the invariant.

                                                                                  Equations
                                                                                  Instances For
                                                                                    @[specialize #[]]
                                                                                    def Batteries.RBNode.insert {α : Type u_1} (cmp : ααOrdering) (t : Batteries.RBNode α) (v : α) :

                                                                                    insert cmp t v inserts element v into the tree, using the provided comparator cmp to put it in the right place and automatically rebalancing the tree as necessary.

                                                                                    Equations
                                                                                    Instances For

                                                                                      Recolor the root of the tree to red if possible.

                                                                                      Equations
                                                                                      Instances For

                                                                                        Rebalancing a tree which has shrunk on the left.

                                                                                        Equations
                                                                                        Instances For

                                                                                          Rebalancing a tree which has shrunk on the right.

                                                                                          Equations
                                                                                          Instances For

                                                                                            The number of nodes in the tree.

                                                                                            Equations
                                                                                            Instances For
                                                                                              @[irreducible]

                                                                                              Concatenate two trees with the same black-height.

                                                                                              Equations
                                                                                              • One or more equations did not get rendered due to their size.
                                                                                              • Batteries.RBNode.nil.append x = x
                                                                                              • x.append Batteries.RBNode.nil = x
                                                                                              Instances For

                                                                                                erase #

                                                                                                @[specialize #[]]
                                                                                                def Batteries.RBNode.del {α : Type u_1} (cut : αOrdering) :

                                                                                                The core of the erase function. The tree returned from this function has a broken invariant, which is restored in erase.

                                                                                                Equations
                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                • Batteries.RBNode.del cut Batteries.RBNode.nil = Batteries.RBNode.nil
                                                                                                Instances For
                                                                                                  @[specialize #[]]
                                                                                                  def Batteries.RBNode.erase {α : Type u_1} (cut : αOrdering) (t : Batteries.RBNode α) :

                                                                                                  The erase cut t function removes an element from the tree t. The cut function is used to locate an element in the tree: it returns .gt if we go too high and .lt if we go too low; if it returns .eq we will remove the element. (The function cmp k for some key k is a valid cut function, but we can also use cuts that are not of this form as long as they are suitably monotonic.)

                                                                                                  Equations
                                                                                                  Instances For
                                                                                                    @[specialize #[]]
                                                                                                    def Batteries.RBNode.find? {α : Type u_1} (cut : αOrdering) :

                                                                                                    Finds an element in the tree satisfying the cut function.

                                                                                                    Equations
                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                    • Batteries.RBNode.find? cut Batteries.RBNode.nil = none
                                                                                                    Instances For
                                                                                                      @[specialize #[]]
                                                                                                      def Batteries.RBNode.upperBound? {α : Type u_1} (cut : αOrdering) :
                                                                                                      Batteries.RBNode αoptParam (Option α) noneOption α

                                                                                                      upperBound? cut retrieves the smallest entry larger than or equal to cut, if it exists.

                                                                                                      Equations
                                                                                                      Instances For
                                                                                                        @[specialize #[]]
                                                                                                        def Batteries.RBNode.lowerBound? {α : Type u_1} (cut : αOrdering) :
                                                                                                        Batteries.RBNode αoptParam (Option α) noneOption α

                                                                                                        lowerBound? cut retrieves the largest entry smaller than or equal to cut, if it exists.

                                                                                                        Equations
                                                                                                        Instances For

                                                                                                          Returns the root of the tree, if any.

                                                                                                          Equations
                                                                                                          Instances For
                                                                                                            @[specialize #[]]
                                                                                                            def Batteries.RBNode.map {α : Type u_1} {β : Type u_2} (f : αβ) :

                                                                                                            O(n). Map a function on every value in the tree. This requires IsMonotone on the function in order to preserve the order invariant.

                                                                                                            Equations
                                                                                                            Instances For

                                                                                                              Converts the tree into an array in increasing sorted order.

                                                                                                              Equations
                                                                                                              Instances For
                                                                                                                inductive Batteries.RBNode.Path (α : Type u) :

                                                                                                                A RBNode.Path α is a "cursor" into an RBNode which represents the path from the root to a subtree. Note that the path goes from the target subtree up to the root, which is reversed from the normal way data is stored in the tree. See Zipper for more information.

                                                                                                                Instances For

                                                                                                                  Fills the Path with a subtree.

                                                                                                                  Equations
                                                                                                                  Instances For
                                                                                                                    @[specialize #[]]
                                                                                                                    def Batteries.RBNode.zoom {α : Type u_1} (cut : αOrdering) :

                                                                                                                    Like find?, but instead of just returning the element, it returns the entire subtree at the element and a path back to the root for reconstructing the tree.

                                                                                                                    Equations
                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                    • Batteries.RBNode.zoom cut Batteries.RBNode.nil x = (Batteries.RBNode.nil, x)
                                                                                                                    Instances For

                                                                                                                      This function does the second part of RBNode.ins, which unwinds the stack and rebuilds the tree.

                                                                                                                      Equations
                                                                                                                      Instances For
                                                                                                                        @[inline]

                                                                                                                        path.insertNew v inserts element v into the tree, assuming that path is zoomed in on a nil node such that inserting a new element at this position is valid.

                                                                                                                        Equations
                                                                                                                        Instances For

                                                                                                                          path.insert t v inserts element v into the tree, assuming that (t, path) was the result of a previous zoom operation (so either the root of t is equivalent to v or it is empty).

                                                                                                                          Equations
                                                                                                                          Instances For

                                                                                                                            path.del t c does the second part of RBNode.del, which unwinds the stack and rebuilds the tree. The c argument is the color of the node before the deletion (we used t₀.isBlack for this in RBNode.del but the original tree is no longer available in this formulation).

                                                                                                                            Equations
                                                                                                                            Instances For

                                                                                                                              path.erase t v removes the root element of t from the tree, assuming that (t, path) was the result of a previous zoom operation.

                                                                                                                              Equations
                                                                                                                              • path.erase Batteries.RBNode.nil = path.fill Batteries.RBNode.nil
                                                                                                                              • path.erase (Batteries.RBNode.node a a_1 a_2 a_3) = path.del (a_1.append a_3) a
                                                                                                                              Instances For
                                                                                                                                @[specialize #[]]
                                                                                                                                def Batteries.RBNode.modify {α : Type u_1} (cut : αOrdering) (f : αα) (t : Batteries.RBNode α) :

                                                                                                                                modify cut f t uses cut to find an element, then modifies the element using f and reinserts it into the tree.

                                                                                                                                Because the tree structure is not modified, f must not modify the ordering properties of the element.

                                                                                                                                The element in t is used linearly if t is unshared.

                                                                                                                                Equations
                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                Instances For
                                                                                                                                  @[specialize #[]]
                                                                                                                                  def Batteries.RBNode.alter {α : Type u_1} (cut : αOrdering) (f : Option αOption α) (t : Batteries.RBNode α) :

                                                                                                                                  alter cut f t simultaneously handles inserting, erasing and replacing an element using a function f : Option α → Option α. It is passed the result of t.find? cut and can either return none to remove the element or some a to replace/insert the element with a (which must have the same ordering properties as the original element).

                                                                                                                                  The element is used linearly if t is unshared.

                                                                                                                                  Equations
                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                  Instances For
                                                                                                                                    def Batteries.RBNode.Ordered {α : Type u_1} (cmp : ααOrdering) :

                                                                                                                                    The ordering invariant of a red-black tree, which is a binary search tree. This says that every element of a left subtree is less than the root, and every element in the right subtree is greater than the root, where the less than relation x < y is understood to mean cmp x y = .lt.

                                                                                                                                    Because we do not assume that cmp is lawful when stating this property, we write it in such a way that if cmp is not lawful then the condition holds trivially. That way we can prove the ordering invariants without assuming cmp is lawful.

                                                                                                                                    Equations
                                                                                                                                    Instances For
                                                                                                                                      Equations
                                                                                                                                      Instances For

                                                                                                                                        The red-black balance invariant. Balanced t c n says that the color of the root node is c, and the black-height (the number of black nodes on any path from the root) of the tree is n. Additionally, every red node must have black children.

                                                                                                                                        Instances For
                                                                                                                                          inductive Batteries.RBNode.WF {α : Type u_1} (cmp : ααOrdering) :

                                                                                                                                          The well-formedness invariant for a red-black tree. The first constructor is the real invariant, and the others allow us to "cheat" in this file and define insert and erase, which have more complex proofs that are delayed to Batteries.Data.RBMap.Lemmas.

                                                                                                                                          Instances For
                                                                                                                                            def Batteries.RBSet (α : Type u) (cmp : ααOrdering) :

                                                                                                                                            An RBSet is a self-balancing binary search tree. The cmp function is the comparator that will be used for performing searches; it should satisfy the requirements of TransCmp for it to have sensible behavior.

                                                                                                                                            Equations
                                                                                                                                            Instances For
                                                                                                                                              @[inline]
                                                                                                                                              def Batteries.mkRBSet (α : Type u) (cmp : ααOrdering) :

                                                                                                                                              O(1). Construct a new empty tree.

                                                                                                                                              Equations
                                                                                                                                              Instances For
                                                                                                                                                @[inline]
                                                                                                                                                def Batteries.RBSet.empty {α : Type u_1} {cmp : ααOrdering} :

                                                                                                                                                O(1). Construct a new empty tree.

                                                                                                                                                Equations
                                                                                                                                                Instances For
                                                                                                                                                  instance Batteries.RBSet.instEmptyCollection (α : Type u) (cmp : ααOrdering) :
                                                                                                                                                  Equations
                                                                                                                                                  instance Batteries.RBSet.instInhabited (α : Type u) (cmp : ααOrdering) :
                                                                                                                                                  Equations
                                                                                                                                                  @[inline]
                                                                                                                                                  def Batteries.RBSet.single {α : Type u_1} {cmp : ααOrdering} (v : α) :

                                                                                                                                                  O(1). Construct a new tree with one element v.

                                                                                                                                                  Equations
                                                                                                                                                  Instances For
                                                                                                                                                    @[inline]
                                                                                                                                                    def Batteries.RBSet.foldl {σ : Sort u_1} {α : Type u_2} {cmp : ααOrdering} (f : σασ) (init : σ) (t : Batteries.RBSet α cmp) :
                                                                                                                                                    σ

                                                                                                                                                    O(n). Fold a function on the values from left to right (in increasing order).

                                                                                                                                                    Equations
                                                                                                                                                    Instances For
                                                                                                                                                      @[inline]
                                                                                                                                                      def Batteries.RBSet.foldr {α : Type u_1} {σ : Sort u_2} {cmp : ααOrdering} (f : ασσ) (init : σ) (t : Batteries.RBSet α cmp) :
                                                                                                                                                      σ

                                                                                                                                                      O(n). Fold a function on the values from right to left (in decreasing order).

                                                                                                                                                      Equations
                                                                                                                                                      Instances For
                                                                                                                                                        @[inline]
                                                                                                                                                        def Batteries.RBSet.foldlM {m : Type u_1 → Type u_2} {σ : Type u_1} {α : Type u_3} {cmp : ααOrdering} [Monad m] (f : σαm σ) (init : σ) (t : Batteries.RBSet α cmp) :
                                                                                                                                                        m σ

                                                                                                                                                        O(n). Fold a monadic function on the values from left to right (in increasing order).

                                                                                                                                                        Equations
                                                                                                                                                        Instances For
                                                                                                                                                          @[inline]
                                                                                                                                                          def Batteries.RBSet.forM {m : Type u_1 → Type u_2} {α : Type u_3} {cmp : ααOrdering} [Monad m] (f : αm PUnit) (t : Batteries.RBSet α cmp) :

                                                                                                                                                          O(n). Run monadic function f on each element of the tree (in increasing order).

                                                                                                                                                          Equations
                                                                                                                                                          Instances For
                                                                                                                                                            instance Batteries.RBSet.instForIn {m : Type u_1 → Type u_2} {α : Type u_3} {cmp : ααOrdering} :
                                                                                                                                                            ForIn m (Batteries.RBSet α cmp) α
                                                                                                                                                            Equations
                                                                                                                                                            instance Batteries.RBSet.instToStreamStream {α : Type u_1} {cmp : ααOrdering} :
                                                                                                                                                            Equations
                                                                                                                                                            • Batteries.RBSet.instToStreamStream = { toStream := fun (x : Batteries.RBSet α cmp) => x.val.toStream }
                                                                                                                                                            @[inline]
                                                                                                                                                            def Batteries.RBSet.isEmpty {α : Type u_1} {cmp : ααOrdering} :

                                                                                                                                                            O(1). Is the tree empty?

                                                                                                                                                            Equations
                                                                                                                                                            Instances For
                                                                                                                                                              @[inline]
                                                                                                                                                              def Batteries.RBSet.toList {α : Type u_1} {cmp : ααOrdering} (t : Batteries.RBSet α cmp) :
                                                                                                                                                              List α

                                                                                                                                                              O(n). Convert the tree to a list in ascending order.

                                                                                                                                                              Equations
                                                                                                                                                              • t.toList = t.val.toList
                                                                                                                                                              Instances For
                                                                                                                                                                @[inline]
                                                                                                                                                                def Batteries.RBSet.min? {α : Type u_1} {cmp : ααOrdering} (t : Batteries.RBSet α cmp) :

                                                                                                                                                                O(log n). Returns the entry a such that a ≤ k for all keys in the RBSet.

                                                                                                                                                                Equations
                                                                                                                                                                • t.min? = t.val.min?
                                                                                                                                                                Instances For
                                                                                                                                                                  @[inline]
                                                                                                                                                                  def Batteries.RBSet.max? {α : Type u_1} {cmp : ααOrdering} (t : Batteries.RBSet α cmp) :

                                                                                                                                                                  O(log n). Returns the entry a such that a ≥ k for all keys in the RBSet.

                                                                                                                                                                  Equations
                                                                                                                                                                  • t.max? = t.val.max?
                                                                                                                                                                  Instances For
                                                                                                                                                                    @[deprecated Batteries.RBSet.min?]
                                                                                                                                                                    def Batteries.RBSet.min {α : Type u_1} {cmp : ααOrdering} (t : Batteries.RBSet α cmp) :

                                                                                                                                                                    Alias of Batteries.RBSet.min?.


                                                                                                                                                                    O(log n). Returns the entry a such that a ≤ k for all keys in the RBSet.

                                                                                                                                                                    Equations
                                                                                                                                                                    Instances For
                                                                                                                                                                      @[deprecated Batteries.RBSet.max?]
                                                                                                                                                                      def Batteries.RBSet.max {α : Type u_1} {cmp : ααOrdering} (t : Batteries.RBSet α cmp) :

                                                                                                                                                                      Alias of Batteries.RBSet.max?.


                                                                                                                                                                      O(log n). Returns the entry a such that a ≥ k for all keys in the RBSet.

                                                                                                                                                                      Equations
                                                                                                                                                                      Instances For
                                                                                                                                                                        instance Batteries.RBSet.instRepr {α : Type u_1} {cmp : ααOrdering} [Repr α] :
                                                                                                                                                                        Equations
                                                                                                                                                                        @[inline]
                                                                                                                                                                        def Batteries.RBSet.insert {α : Type u_1} {cmp : ααOrdering} (t : Batteries.RBSet α cmp) (v : α) :

                                                                                                                                                                        O(log n). Insert element v into the tree.

                                                                                                                                                                        Equations
                                                                                                                                                                        Instances For
                                                                                                                                                                          def Batteries.RBSet.insertMany {ρ : Type u_1} {α : Type u_2} {cmp : ααOrdering} [ForIn Id ρ α] (s : Batteries.RBSet α cmp) (as : ρ) :

                                                                                                                                                                          Insert all elements from a collection into a RBSet α cmp.

                                                                                                                                                                          Equations
                                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                                          Instances For
                                                                                                                                                                            @[inline]
                                                                                                                                                                            def Batteries.RBSet.erase {α : Type u_1} {cmp : ααOrdering} (t : Batteries.RBSet α cmp) (cut : αOrdering) :

                                                                                                                                                                            O(log n). Remove an element from the tree using a cut function. The cut function is used to locate an element in the tree: it returns .gt if we go too high and .lt if we go too low; if it returns .eq we will remove the element. (The function cmp k for some key k is a valid cut function, but we can also use cuts that are not of this form as long as they are suitably monotonic.)

                                                                                                                                                                            Equations
                                                                                                                                                                            Instances For
                                                                                                                                                                              @[inline]
                                                                                                                                                                              def Batteries.RBSet.findP? {α : Type u_1} {cmp : ααOrdering} (t : Batteries.RBSet α cmp) (cut : αOrdering) :

                                                                                                                                                                              O(log n). Find an element in the tree using a cut function.

                                                                                                                                                                              Equations
                                                                                                                                                                              Instances For
                                                                                                                                                                                @[inline]
                                                                                                                                                                                def Batteries.RBSet.find? {α : Type u_1} {cmp : ααOrdering} (t : Batteries.RBSet α cmp) (x : α) :

                                                                                                                                                                                O(log n). Returns an element in the tree equivalent to x if one exists.

                                                                                                                                                                                Equations
                                                                                                                                                                                Instances For
                                                                                                                                                                                  @[inline]
                                                                                                                                                                                  def Batteries.RBSet.findPD {α : Type u_1} {cmp : ααOrdering} (t : Batteries.RBSet α cmp) (cut : αOrdering) (v₀ : α) :
                                                                                                                                                                                  α

                                                                                                                                                                                  O(log n). Find an element in the tree, or return a default value v₀.

                                                                                                                                                                                  Equations
                                                                                                                                                                                  • t.findPD cut v₀ = (t.findP? cut).getD v₀
                                                                                                                                                                                  Instances For
                                                                                                                                                                                    @[inline]
                                                                                                                                                                                    def Batteries.RBSet.upperBoundP? {α : Type u_1} {cmp : ααOrdering} (t : Batteries.RBSet α cmp) (cut : αOrdering) :

                                                                                                                                                                                    O(log n). upperBoundP cut retrieves the smallest entry comparing gt or eq under cut, if it exists. If multiple keys in the map return eq under cut, any of them may be returned.

                                                                                                                                                                                    Equations
                                                                                                                                                                                    Instances For
                                                                                                                                                                                      @[inline]
                                                                                                                                                                                      def Batteries.RBSet.upperBound? {α : Type u_1} {cmp : ααOrdering} (t : Batteries.RBSet α cmp) (k : α) :

                                                                                                                                                                                      O(log n). upperBound? k retrieves the largest entry smaller than or equal to k, if it exists.

                                                                                                                                                                                      Equations
                                                                                                                                                                                      • t.upperBound? k = t.upperBoundP? (cmp k)
                                                                                                                                                                                      Instances For
                                                                                                                                                                                        @[inline]
                                                                                                                                                                                        def Batteries.RBSet.lowerBoundP? {α : Type u_1} {cmp : ααOrdering} (t : Batteries.RBSet α cmp) (cut : αOrdering) :

                                                                                                                                                                                        O(log n). lowerBoundP cut retrieves the largest entry comparing lt or eq under cut, if it exists. If multiple keys in the map return eq under cut, any of them may be returned.

                                                                                                                                                                                        Equations
                                                                                                                                                                                        Instances For
                                                                                                                                                                                          @[inline]
                                                                                                                                                                                          def Batteries.RBSet.lowerBound? {α : Type u_1} {cmp : ααOrdering} (t : Batteries.RBSet α cmp) (k : α) :

                                                                                                                                                                                          O(log n). lowerBound? k retrieves the largest entry smaller than or equal to k, if it exists.

                                                                                                                                                                                          Equations
                                                                                                                                                                                          • t.lowerBound? k = t.lowerBoundP? (cmp k)
                                                                                                                                                                                          Instances For
                                                                                                                                                                                            @[inline]
                                                                                                                                                                                            def Batteries.RBSet.containsP {α : Type u_1} {cmp : ααOrdering} (t : Batteries.RBSet α cmp) (cut : αOrdering) :

                                                                                                                                                                                            O(log n). Returns true if the given cut returns eq for something in the RBSet.

                                                                                                                                                                                            Equations
                                                                                                                                                                                            • t.containsP cut = (t.findP? cut).isSome
                                                                                                                                                                                            Instances For
                                                                                                                                                                                              @[inline]
                                                                                                                                                                                              def Batteries.RBSet.contains {α : Type u_1} {cmp : ααOrdering} (t : Batteries.RBSet α cmp) (a : α) :

                                                                                                                                                                                              O(log n). Returns true if the given key a is in the RBSet.

                                                                                                                                                                                              Equations
                                                                                                                                                                                              • t.contains a = (t.find? a).isSome
                                                                                                                                                                                              Instances For
                                                                                                                                                                                                @[inline]
                                                                                                                                                                                                def Batteries.RBSet.ofList {α : Type u_1} (l : List α) (cmp : ααOrdering) :

                                                                                                                                                                                                O(n log n). Build a tree from an unsorted list by inserting them one at a time.

                                                                                                                                                                                                Equations
                                                                                                                                                                                                Instances For
                                                                                                                                                                                                  @[inline]
                                                                                                                                                                                                  def Batteries.RBSet.ofArray {α : Type u_1} (l : Array α) (cmp : ααOrdering) :

                                                                                                                                                                                                  O(n log n). Build a tree from an unsorted array by inserting them one at a time.

                                                                                                                                                                                                  Equations
                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                    @[inline]
                                                                                                                                                                                                    def Batteries.RBSet.all {α : Type u_1} {cmp : ααOrdering} (t : Batteries.RBSet α cmp) (p : αBool) :

                                                                                                                                                                                                    O(n). Returns true if the given predicate is true for all items in the RBSet.

                                                                                                                                                                                                    Equations
                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                      @[inline]
                                                                                                                                                                                                      def Batteries.RBSet.any {α : Type u_1} {cmp : ααOrdering} (t : Batteries.RBSet α cmp) (p : αBool) :

                                                                                                                                                                                                      O(n). Returns true if the given predicate is true for any item in the RBSet.

                                                                                                                                                                                                      Equations
                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                        @[inline]
                                                                                                                                                                                                        def Batteries.RBSet.all₂ {α : Type u_1} {β : Type u_2} {cmpα : ααOrdering} {cmpβ : ββOrdering} (R : αβBool) (t₁ : Batteries.RBSet α cmpα) (t₂ : Batteries.RBSet β cmpβ) :

                                                                                                                                                                                                        Asserts that t₁ and t₂ have the same number of elements in the same order, and R holds pairwise between them. The tree structure is ignored.

                                                                                                                                                                                                        Equations
                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                          def Batteries.RBSet.EMem {α : Type u_1} {cmp : ααOrdering} (x : α) (t : Batteries.RBSet α cmp) :

                                                                                                                                                                                                          True if x is an element of t "exactly", i.e. up to equality, not the cmp relation.

                                                                                                                                                                                                          Equations
                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                            def Batteries.RBSet.MemP {α : Type u_1} {cmp : ααOrdering} (cut : αOrdering) (t : Batteries.RBSet α cmp) :

                                                                                                                                                                                                            True if the specified cut matches at least one element of of t.

                                                                                                                                                                                                            Equations
                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                              def Batteries.RBSet.Mem {α : Type u_1} {cmp : ααOrdering} (x : α) (t : Batteries.RBSet α cmp) :

                                                                                                                                                                                                              True if x is equivalent to an element of t.

                                                                                                                                                                                                              Equations
                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                instance Batteries.RBSet.instMembership {α : Type u_1} {cmp : ααOrdering} :
                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                def Batteries.RBSet.Slow.instDecidableEMem {α : Type u_1} {cmp : ααOrdering} {x : α} [DecidableEq α] {t : Batteries.RBSet α cmp} :
                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                  def Batteries.RBSet.Slow.instDecidableMemP {α : Type u_1} {cmp : ααOrdering} {cut : αOrdering} {t : Batteries.RBSet α cmp} :
                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                    def Batteries.RBSet.Slow.instDecidableMem {α : Type u_1} {cmp : ααOrdering} {x : α} {t : Batteries.RBSet α cmp} :
                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                      instance Batteries.RBSet.instBEq {α : Type u_1} {cmp : ααOrdering} [BEq α] :

                                                                                                                                                                                                                      Returns true if t₁ and t₂ are equal as sets (assuming cmp and == are compatible), ignoring the internal tree structure.

                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                      def Batteries.RBSet.size {α : Type u_1} {cmp : ααOrdering} (m : Batteries.RBSet α cmp) :

                                                                                                                                                                                                                      O(n). The number of items in the RBSet.

                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                      • m.size = m.val.size
                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                        @[inline]
                                                                                                                                                                                                                        def Batteries.RBSet.min! {α : Type u_1} {cmp : ααOrdering} [Inhabited α] (t : Batteries.RBSet α cmp) :
                                                                                                                                                                                                                        α

                                                                                                                                                                                                                        O(log n). Returns the minimum element of the tree, or panics if the tree is empty.

                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                        • t.min! = t.min?.getD (panicWithPosWithDecl "Batteries.Data.RBMap.Basic" "Batteries.RBSet.min!" 798 71 "tree is empty")
                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                          @[inline]
                                                                                                                                                                                                                          def Batteries.RBSet.max! {α : Type u_1} {cmp : ααOrdering} [Inhabited α] (t : Batteries.RBSet α cmp) :
                                                                                                                                                                                                                          α

                                                                                                                                                                                                                          O(log n). Returns the maximum element of the tree, or panics if the tree is empty.

                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                          • t.max! = t.max?.getD (panicWithPosWithDecl "Batteries.Data.RBMap.Basic" "Batteries.RBSet.max!" 801 71 "tree is empty")
                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                            @[inline]
                                                                                                                                                                                                                            def Batteries.RBSet.findP! {α : Type u_1} {cmp : ααOrdering} [Inhabited α] (t : Batteries.RBSet α cmp) (cut : αOrdering) :
                                                                                                                                                                                                                            α

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

                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                            • t.findP! cut = (t.findP? cut).getD (panicWithPosWithDecl "Batteries.Data.RBMap.Basic" "Batteries.RBSet.findP!" 807 23 "key is not in the tree")
                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                              @[inline]
                                                                                                                                                                                                                              def Batteries.RBSet.find! {α : Type u_1} {cmp : ααOrdering} [Inhabited α] (t : Batteries.RBSet α cmp) (k : α) :
                                                                                                                                                                                                                              α

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

                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                              • t.find! k = (t.find? k).getD (panicWithPosWithDecl "Batteries.Data.RBMap.Basic" "Batteries.RBSet.find!" 813 20 "key is not in the tree")
                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                class Batteries.RBSet.ModifyWF {α : Type u_1} {cmp : ααOrdering} (t : Batteries.RBSet α cmp) (cut : αOrdering) (f : αα) :

                                                                                                                                                                                                                                The predicate asserting that the result of modifyP is safe to construct.

                                                                                                                                                                                                                                Instances
                                                                                                                                                                                                                                  theorem Batteries.RBSet.ModifyWF.wf {α : Type u_1} {cmp : ααOrdering} {t : Batteries.RBSet α cmp} {cut : αOrdering} {f : αα} [self : t.ModifyWF cut f] :

                                                                                                                                                                                                                                  The resulting tree is well formed.

                                                                                                                                                                                                                                  def Batteries.RBSet.modifyP {α : Type u_1} {cmp : ααOrdering} (t : Batteries.RBSet α cmp) (cut : αOrdering) (f : αα) [wf : t.ModifyWF cut f] :

                                                                                                                                                                                                                                  O(log n). In-place replace an element found by cut. This takes the element out of the tree while f runs, so it uses the element linearly if t is unshared.

                                                                                                                                                                                                                                  The ModifyWF assumption is required because f may change the ordering properties of the element, which would break the invariants.

                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                    class Batteries.RBSet.AlterWF {α : Type u_1} {cmp : ααOrdering} (t : Batteries.RBSet α cmp) (cut : αOrdering) (f : Option αOption α) :

                                                                                                                                                                                                                                    The predicate asserting that the result of alterP is safe to construct.

                                                                                                                                                                                                                                    Instances
                                                                                                                                                                                                                                      theorem Batteries.RBSet.AlterWF.wf {α : Type u_1} {cmp : ααOrdering} {t : Batteries.RBSet α cmp} {cut : αOrdering} {f : Option αOption α} [self : t.AlterWF cut f] :

                                                                                                                                                                                                                                      The resulting tree is well formed.

                                                                                                                                                                                                                                      def Batteries.RBSet.alterP {α : Type u_1} {cmp : ααOrdering} (t : Batteries.RBSet α cmp) (cut : αOrdering) (f : Option αOption α) [wf : t.AlterWF cut f] :

                                                                                                                                                                                                                                      O(log n). alterP cut f t simultaneously handles inserting, erasing and replacing an element using a function f : Option α → Option α. It is passed the result of t.findP? cut and can either return none to remove the element or some a to replace/insert the element with a (which must have the same ordering properties as the original element).

                                                                                                                                                                                                                                      The element is used linearly if t is unshared.

                                                                                                                                                                                                                                      The AlterWF assumption is required because f may change the ordering properties of the element, which would break the invariants.

                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                        def Batteries.RBSet.union {α : Type u_1} {cmp : ααOrdering} (t₁ : Batteries.RBSet α cmp) (t₂ : Batteries.RBSet α cmp) :

                                                                                                                                                                                                                                        O(n₂ * log (n₁ + n₂)). Merges the maps t₁ and t₂. If equal keys exist in both, the key from t₂ is preferred.

                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                          instance Batteries.RBSet.instUnion {α : Type u_1} {cmp : ααOrdering} :
                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                          • Batteries.RBSet.instUnion = { union := Batteries.RBSet.union }
                                                                                                                                                                                                                                          def Batteries.RBSet.mergeWith {α : Type u_1} {cmp : ααOrdering} (mergeFn : ααα) (t₁ : Batteries.RBSet α cmp) (t₂ : Batteries.RBSet α cmp) :

                                                                                                                                                                                                                                          O(n₂ * log (n₁ + n₂)). Merges the maps t₁ and t₂. If equal keys exist in both, then use mergeFn a₁ a₂ to produce the new merged value.

                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                            def Batteries.RBSet.intersectWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} {cmpα : ααOrdering} {cmpβ : ββOrdering} {cmpγ : γγOrdering} (cmp : αβOrdering) (mergeFn : αβγ) (t₁ : Batteries.RBSet α cmpα) (t₂ : Batteries.RBSet β cmpβ) :

                                                                                                                                                                                                                                            O(n₁ * log (n₁ + n₂)). Intersects the maps t₁ and t₂ using mergeFn a b to produce the new value.

                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                              def Batteries.RBSet.filter {α : Type u_1} {cmp : ααOrdering} (t : Batteries.RBSet α cmp) (p : αBool) :

                                                                                                                                                                                                                                              O(n * log n). Constructs the set of all elements satisfying p.

                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                def Batteries.RBSet.map {α : Type u_1} {cmpα : ααOrdering} {β : Type u_2} {cmpβ : ββOrdering} (t : Batteries.RBSet α cmpα) (f : αβ) :

                                                                                                                                                                                                                                                O(n * log n). Map a function on every value in the set. If the function is monotone, consider using the more efficient RBSet.mapMonotone instead.

                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                  def Batteries.RBSet.sdiff {α : Type u_1} {cmp : ααOrdering} (t₁ : Batteries.RBSet α cmp) (t₂ : Batteries.RBSet α cmp) :

                                                                                                                                                                                                                                                  O(n₁ * (log n₁ + log n₂)). Constructs the set of all elements of t₁ that are not in t₂.

                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                  • t₁.sdiff t₂ = t₁.filter fun (x : α) => !t₂.contains x
                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                    instance Batteries.RBSet.instSDiff {α : Type u_1} {cmp : ααOrdering} :
                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                    • Batteries.RBSet.instSDiff = { sdiff := Batteries.RBSet.sdiff }
                                                                                                                                                                                                                                                    def Batteries.RBMap (α : Type u) (β : Type v) (cmp : ααOrdering) :
                                                                                                                                                                                                                                                    Type (max u v)

                                                                                                                                                                                                                                                    An RBMap is a self-balancing binary search tree, used to store a key-value map. The cmp function is the comparator that will be used for performing searches; it should satisfy the requirements of TransCmp for it to have sensible behavior.

                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                      @[inline]
                                                                                                                                                                                                                                                      def Batteries.mkRBMap (α : Type u) (β : Type v) (cmp : ααOrdering) :
                                                                                                                                                                                                                                                      Batteries.RBMap α β cmp

                                                                                                                                                                                                                                                      O(1). Construct a new empty map.

                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                        @[inline]
                                                                                                                                                                                                                                                        def Batteries.RBMap.empty {α : Type u} {β : Type v} {cmp : ααOrdering} :
                                                                                                                                                                                                                                                        Batteries.RBMap α β cmp

                                                                                                                                                                                                                                                        O(1). Construct a new empty map.

                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                          instance Batteries.instEmptyCollectionRBMap (α : Type u) (β : Type v) (cmp : ααOrdering) :
                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                          instance Batteries.instInhabitedRBMap (α : Type u) (β : Type v) (cmp : ααOrdering) :
                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                          @[inline]
                                                                                                                                                                                                                                                          def Batteries.RBMap.single {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} (k : α) (v : β) :
                                                                                                                                                                                                                                                          Batteries.RBMap α β cmp

                                                                                                                                                                                                                                                          O(1). Construct a new tree with one key-value pair k, v.

                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                            @[inline]
                                                                                                                                                                                                                                                            def Batteries.RBMap.foldl {α : Type u} {β : Type v} {σ : Type w} {cmp : ααOrdering} (f : σαβσ) (init : σ) :
                                                                                                                                                                                                                                                            Batteries.RBMap α β cmpσ

                                                                                                                                                                                                                                                            O(n). Fold a function on the values from left to right (in increasing order).

                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                              @[inline]
                                                                                                                                                                                                                                                              def Batteries.RBMap.foldr {α : Type u} {β : Type v} {σ : Type w} {cmp : ααOrdering} (f : αβσσ) (init : σ) :
                                                                                                                                                                                                                                                              Batteries.RBMap α β cmpσ

                                                                                                                                                                                                                                                              O(n). Fold a function on the values from right to left (in decreasing order).

                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                @[inline]
                                                                                                                                                                                                                                                                def Batteries.RBMap.foldlM {α : Type u} {β : Type v} {σ : Type w} {cmp : ααOrdering} {m : Type w → Type u_1} [Monad m] (f : σαβm σ) (init : σ) :
                                                                                                                                                                                                                                                                Batteries.RBMap α β cmpm σ

                                                                                                                                                                                                                                                                O(n). Fold a monadic function on the values from left to right (in increasing order).

                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                  @[inline]
                                                                                                                                                                                                                                                                  def Batteries.RBMap.forM {α : Type u} {β : Type v} {cmp : ααOrdering} {m : Type u_1 → Type u_2} [Monad m] (f : αβm PUnit) (t : Batteries.RBMap α β cmp) :

                                                                                                                                                                                                                                                                  O(n). Run monadic function f on each element of the tree (in increasing order).

                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                    instance Batteries.RBMap.instForInProd {α : Type u} {β : Type v} {cmp : ααOrdering} {m : Type u_1 → Type u_2} :
                                                                                                                                                                                                                                                                    ForIn m (Batteries.RBMap α β cmp) (α × β)
                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                    instance Batteries.RBMap.instToStreamStreamProd {α : Type u} {β : Type v} {cmp : ααOrdering} :
                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                    @[inline]
                                                                                                                                                                                                                                                                    def Batteries.RBMap.keysArray {α : Type u} {β : Type v} {cmp : ααOrdering} (t : Batteries.RBMap α β cmp) :

                                                                                                                                                                                                                                                                    O(n). Constructs the array of keys of the map.

                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                      @[inline]
                                                                                                                                                                                                                                                                      def Batteries.RBMap.keysList {α : Type u} {β : Type v} {cmp : ααOrdering} (t : Batteries.RBMap α β cmp) :
                                                                                                                                                                                                                                                                      List α

                                                                                                                                                                                                                                                                      O(n). Constructs the list of keys of the map.

                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                        def Batteries.RBMap.Keys (α : Type u_1) (β : Type u_2) (cmp : ααOrdering) :
                                                                                                                                                                                                                                                                        Type (max u_1 u_2)

                                                                                                                                                                                                                                                                        An "iterator" over the keys of the map. This is a trivial wrapper over the underlying map, but it comes with a small API to use it in a for loop or convert it to an array or list.

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

                                                                                                                                                                                                                                                                          The keys of the map. This is an O(1) wrapper operation, which can be used in for loops or converted to an array or list.

                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                          • t.keys = t
                                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                                            @[inline]
                                                                                                                                                                                                                                                                            def Batteries.RBMap.Keys.toArray {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} (t : Batteries.RBMap α β cmp) :

                                                                                                                                                                                                                                                                            O(n). Constructs the array of keys of the map.

                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                              @[inline]
                                                                                                                                                                                                                                                                              def Batteries.RBMap.Keys.toList {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} (t : Batteries.RBMap α β cmp) :
                                                                                                                                                                                                                                                                              List α

                                                                                                                                                                                                                                                                              O(n). Constructs the list of keys of the map.

                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                                instance Batteries.RBMap.instCoeHeadKeysArray {α : Type u} {β : Type v} {cmp : ααOrdering} :
                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                • Batteries.RBMap.instCoeHeadKeysArray = { coe := Batteries.RBMap.keysArray }
                                                                                                                                                                                                                                                                                instance Batteries.RBMap.instCoeHeadKeysList {α : Type u} {β : Type v} {cmp : ααOrdering} :
                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                • Batteries.RBMap.instCoeHeadKeysList = { coe := Batteries.RBMap.keysList }
                                                                                                                                                                                                                                                                                instance Batteries.RBMap.instForInKeys {α : Type u} {β : Type v} {cmp : ααOrdering} {m : Type u_1 → Type u_2} :
                                                                                                                                                                                                                                                                                ForIn m (Batteries.RBMap.Keys α β cmp) α
                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                instance Batteries.RBMap.instForMKeys {α : Type u} {β : Type v} {cmp : ααOrdering} {m : Type u_1 → Type u_2} :
                                                                                                                                                                                                                                                                                ForM m (Batteries.RBMap.Keys α β cmp) α
                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                def Batteries.RBMap.Keys.Stream (α : Type u_1) (β : Type u_2) :
                                                                                                                                                                                                                                                                                Type (max u_2 u_1)

                                                                                                                                                                                                                                                                                The result of toStream on a Keys.

                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                  def Batteries.RBMap.Keys.toStream {α : Type u} {β : Type v} {cmp : ααOrdering} (t : Batteries.RBMap.Keys α β cmp) :

                                                                                                                                                                                                                                                                                  A stream over the iterator.

                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                  • t.toStream = t.val.toStream
                                                                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                                                                    O(1) amortized, O(log n) worst case: Get the next element from the stream.

                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                      instance Batteries.RBMap.instToStreamKeysStream {α : Type u} {β : Type v} {cmp : ααOrdering} :
                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                      • Batteries.RBMap.instToStreamKeysStream = { toStream := Batteries.RBMap.Keys.toStream }
                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                      • Batteries.RBMap.instStreamStream = { next? := Batteries.RBMap.Keys.Stream.next? }
                                                                                                                                                                                                                                                                                      @[inline]
                                                                                                                                                                                                                                                                                      def Batteries.RBMap.valuesArray {α : Type u} {β : Type v} {cmp : ααOrdering} (t : Batteries.RBMap α β cmp) :

                                                                                                                                                                                                                                                                                      O(n). Constructs the array of values of the map.

                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                                        @[inline]
                                                                                                                                                                                                                                                                                        def Batteries.RBMap.valuesList {α : Type u} {β : Type v} {cmp : ααOrdering} (t : Batteries.RBMap α β cmp) :
                                                                                                                                                                                                                                                                                        List β

                                                                                                                                                                                                                                                                                        O(n). Constructs the list of values of the map.

                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                          def Batteries.RBMap.Values (α : Type u_1) (β : Type u_2) (cmp : ααOrdering) :
                                                                                                                                                                                                                                                                                          Type (max u_1 u_2)

                                                                                                                                                                                                                                                                                          An "iterator" over the values of the map. This is a trivial wrapper over the underlying map, but it comes with a small API to use it in a for loop or convert it to an array or list.

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

                                                                                                                                                                                                                                                                                            The "keys" of the map. This is an O(1) wrapper operation, which can be used in for loops or converted to an array or list.

                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                            • t.values = t
                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                              @[inline]
                                                                                                                                                                                                                                                                                              def Batteries.RBMap.Values.toArray {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} (t : Batteries.RBMap α β cmp) :

                                                                                                                                                                                                                                                                                              O(n). Constructs the array of values of the map.

                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                                                @[inline]
                                                                                                                                                                                                                                                                                                def Batteries.RBMap.Values.toList {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} (t : Batteries.RBMap α β cmp) :
                                                                                                                                                                                                                                                                                                List β

                                                                                                                                                                                                                                                                                                O(n). Constructs the list of values of the map.

                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                  instance Batteries.RBMap.instCoeHeadValuesArray {α : Type u} {β : Type v} {cmp : ααOrdering} :
                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                  • Batteries.RBMap.instCoeHeadValuesArray = { coe := Batteries.RBMap.valuesArray }
                                                                                                                                                                                                                                                                                                  instance Batteries.RBMap.instCoeHeadValuesList {α : Type u} {β : Type v} {cmp : ααOrdering} :
                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                  • Batteries.RBMap.instCoeHeadValuesList = { coe := Batteries.RBMap.valuesList }
                                                                                                                                                                                                                                                                                                  instance Batteries.RBMap.instForInValues {α : Type u} {β : Type v} {cmp : ααOrdering} {m : Type u_1 → Type u_2} :
                                                                                                                                                                                                                                                                                                  ForIn m (Batteries.RBMap.Values α β cmp) β
                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                  instance Batteries.RBMap.instForMValues {α : Type u} {β : Type v} {cmp : ααOrdering} {m : Type u_1 → Type u_2} :
                                                                                                                                                                                                                                                                                                  ForM m (Batteries.RBMap.Values α β cmp) β
                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                  def Batteries.RBMap.Values.Stream (α : Type u_1) (β : Type u_2) :
                                                                                                                                                                                                                                                                                                  Type (max u_2 u_1)

                                                                                                                                                                                                                                                                                                  The result of toStream on a Values.

                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                                    def Batteries.RBMap.Values.toStream {α : Type u} {β : Type v} {cmp : ααOrdering} (t : Batteries.RBMap.Values α β cmp) :

                                                                                                                                                                                                                                                                                                    A stream over the iterator.

                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                    • t.toStream = t.val.toStream
                                                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                                                      O(1) amortized, O(log n) worst case: Get the next element from the stream.

                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                        • Batteries.RBMap.instToStreamValuesStream = { toStream := Batteries.RBMap.Values.toStream }
                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                        • Batteries.RBMap.instStreamStream_1 = { next? := Batteries.RBMap.Values.Stream.next? }
                                                                                                                                                                                                                                                                                                        @[inline]
                                                                                                                                                                                                                                                                                                        def Batteries.RBMap.isEmpty {α : Type u} {β : Type v} {cmp : ααOrdering} :
                                                                                                                                                                                                                                                                                                        Batteries.RBMap α β cmpBool

                                                                                                                                                                                                                                                                                                        O(1). Is the tree empty?

                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                        • Batteries.RBMap.isEmpty = Batteries.RBSet.isEmpty
                                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                                          @[inline]
                                                                                                                                                                                                                                                                                                          def Batteries.RBMap.toList {α : Type u} {β : Type v} {cmp : ααOrdering} :
                                                                                                                                                                                                                                                                                                          Batteries.RBMap α β cmpList (α × β)

                                                                                                                                                                                                                                                                                                          O(n). Convert the tree to a list in ascending order.

                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                          • Batteries.RBMap.toList = Batteries.RBSet.toList
                                                                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                                                                            @[inline]
                                                                                                                                                                                                                                                                                                            def Batteries.RBMap.min? {α : Type u} {β : Type v} {cmp : ααOrdering} :
                                                                                                                                                                                                                                                                                                            Batteries.RBMap α β cmpOption (α × β)

                                                                                                                                                                                                                                                                                                            O(log n). Returns the key-value pair (a, b) such that a ≤ k for all keys in the RBMap.

                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                            • Batteries.RBMap.min? = Batteries.RBSet.min?
                                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                                              @[inline]
                                                                                                                                                                                                                                                                                                              def Batteries.RBMap.max? {α : Type u} {β : Type v} {cmp : ααOrdering} :
                                                                                                                                                                                                                                                                                                              Batteries.RBMap α β cmpOption (α × β)

                                                                                                                                                                                                                                                                                                              O(log n). Returns the key-value pair (a, b) such that a ≥ k for all keys in the RBMap.

                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                              • Batteries.RBMap.max? = Batteries.RBSet.max?
                                                                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                                                                @[deprecated Batteries.RBMap.min?]
                                                                                                                                                                                                                                                                                                                def Batteries.RBMap.min {α : Type u} {β : Type v} {cmp : ααOrdering} :
                                                                                                                                                                                                                                                                                                                Batteries.RBMap α β cmpOption (α × β)

                                                                                                                                                                                                                                                                                                                Alias of Batteries.RBMap.min?.


                                                                                                                                                                                                                                                                                                                O(log n). Returns the key-value pair (a, b) such that a ≤ k for all keys in the RBMap.

                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                                  @[deprecated Batteries.RBMap.max?]
                                                                                                                                                                                                                                                                                                                  def Batteries.RBMap.max {α : Type u} {β : Type v} {cmp : ααOrdering} :
                                                                                                                                                                                                                                                                                                                  Batteries.RBMap α β cmpOption (α × β)

                                                                                                                                                                                                                                                                                                                  Alias of Batteries.RBMap.max?.


                                                                                                                                                                                                                                                                                                                  O(log n). Returns the key-value pair (a, b) such that a ≥ k for all keys in the RBMap.

                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                                                    instance Batteries.RBMap.instRepr {α : Type u} {β : Type v} {cmp : ααOrdering} [Repr α] [Repr β] :
                                                                                                                                                                                                                                                                                                                    Repr (Batteries.RBMap α β cmp)
                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                    @[inline]
                                                                                                                                                                                                                                                                                                                    def Batteries.RBMap.insert {α : Type u} {β : Type v} {cmp : ααOrdering} (t : Batteries.RBMap α β cmp) (k : α) (v : β) :
                                                                                                                                                                                                                                                                                                                    Batteries.RBMap α β cmp

                                                                                                                                                                                                                                                                                                                    O(log n). Insert key-value pair (k, v) into the tree.

                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                                      @[inline]
                                                                                                                                                                                                                                                                                                                      def Batteries.RBMap.erase {α : Type u} {β : Type v} {cmp : ααOrdering} (t : Batteries.RBMap α β cmp) (k : α) :
                                                                                                                                                                                                                                                                                                                      Batteries.RBMap α β cmp

                                                                                                                                                                                                                                                                                                                      O(log n). Remove an element k from the map.

                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                                                                        @[inline]
                                                                                                                                                                                                                                                                                                                        def Batteries.RBMap.ofList {α : Type u} {β : Type v} (l : List (α × β)) (cmp : ααOrdering) :
                                                                                                                                                                                                                                                                                                                        Batteries.RBMap α β cmp

                                                                                                                                                                                                                                                                                                                        O(n log n). Build a tree from an unsorted list by inserting them one at a time.

                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                                                          @[inline]
                                                                                                                                                                                                                                                                                                                          def Batteries.RBMap.ofArray {α : Type u} {β : Type v} (l : Array (α × β)) (cmp : ααOrdering) :
                                                                                                                                                                                                                                                                                                                          Batteries.RBMap α β cmp

                                                                                                                                                                                                                                                                                                                          O(n log n). Build a tree from an unsorted array by inserting them one at a time.

                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                                                                                            @[inline]
                                                                                                                                                                                                                                                                                                                            def Batteries.RBMap.findEntry? {α : Type u} {β : Type v} {cmp : ααOrdering} (t : Batteries.RBMap α β cmp) (k : α) :
                                                                                                                                                                                                                                                                                                                            Option (α × β)

                                                                                                                                                                                                                                                                                                                            O(log n). Find an entry in the tree with key equal to k.

                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                                                              @[inline]
                                                                                                                                                                                                                                                                                                                              def Batteries.RBMap.find? {α : Type u} {β : Type v} {cmp : ααOrdering} (t : Batteries.RBMap α β cmp) (k : α) :

                                                                                                                                                                                                                                                                                                                              O(log n). Find the value corresponding to key k.

                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                              • t.find? k = Option.map (fun (x : α × β) => x.snd) (t.findEntry? k)
                                                                                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                                                                                @[inline]
                                                                                                                                                                                                                                                                                                                                def Batteries.RBMap.findD {α : Type u} {β : Type v} {cmp : ααOrdering} (t : Batteries.RBMap α β cmp) (k : α) (v₀ : β) :
                                                                                                                                                                                                                                                                                                                                β

                                                                                                                                                                                                                                                                                                                                O(log n). Find the value corresponding to key k, or return v₀ if it is not in the map.

                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                • t.findD k v₀ = (t.find? k).getD v₀
                                                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                                                  @[inline]
                                                                                                                                                                                                                                                                                                                                  def Batteries.RBMap.lowerBound? {α : Type u} {β : Type v} {cmp : ααOrdering} (t : Batteries.RBMap α β cmp) (k : α) :
                                                                                                                                                                                                                                                                                                                                  Option (α × β)

                                                                                                                                                                                                                                                                                                                                  O(log n). lowerBound? k retrieves the key-value pair of the largest key smaller than or equal to k, if it exists.

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

                                                                                                                                                                                                                                                                                                                                    O(log n). Returns true if the given key a is in the RBMap.

                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                    • t.contains a = (t.findEntry? a).isSome
                                                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                                                      @[inline]
                                                                                                                                                                                                                                                                                                                                      def Batteries.RBMap.all {α : Type u} {β : Type v} {cmp : ααOrdering} (t : Batteries.RBMap α β cmp) (p : αβBool) :

                                                                                                                                                                                                                                                                                                                                      O(n). Returns true if the given predicate is true for all items in the RBMap.

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

                                                                                                                                                                                                                                                                                                                                        O(n). Returns true if the given predicate is true for any item in the RBMap.

                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                                                                          @[inline]
                                                                                                                                                                                                                                                                                                                                          def Batteries.RBMap.all₂ {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {cmpα : ααOrdering} {cmpγ : γγOrdering} (R : α × βγ × δBool) (t₁ : Batteries.RBMap α β cmpα) (t₂ : Batteries.RBMap γ δ cmpγ) :

                                                                                                                                                                                                                                                                                                                                          Asserts that t₁ and t₂ have the same number of elements in the same order, and R holds pairwise between them. The tree structure is ignored.

                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                                                                                                            @[inline]
                                                                                                                                                                                                                                                                                                                                            def Batteries.RBMap.eqKeys {α : Type u} {β : Type v} {cmp : ααOrdering} {γ : Type u_1} (t₁ : Batteries.RBMap α β cmp) (t₂ : Batteries.RBMap α γ cmp) :

                                                                                                                                                                                                                                                                                                                                            Asserts that t₁ and t₂ have the same set of keys (up to equality).

                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                                                                              instance Batteries.RBMap.instBEq {α : Type u} {β : Type v} {cmp : ααOrdering} [BEq α] [BEq β] :
                                                                                                                                                                                                                                                                                                                                              BEq (Batteries.RBMap α β cmp)

                                                                                                                                                                                                                                                                                                                                              Returns true if t₁ and t₂ have the same keys and values (assuming cmp and == are compatible), ignoring the internal tree structure.

                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                              def Batteries.RBMap.size {α : Type u} {β : Type v} {cmp : ααOrdering} :
                                                                                                                                                                                                                                                                                                                                              Batteries.RBMap α β cmpNat

                                                                                                                                                                                                                                                                                                                                              O(n). The number of items in the RBMap.

                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                              • Batteries.RBMap.size = Batteries.RBSet.size
                                                                                                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                                                                                                @[inline]
                                                                                                                                                                                                                                                                                                                                                def Batteries.RBMap.min! {α : Type u} {β : Type v} {cmp : ααOrdering} [Inhabited α] [Inhabited β] :
                                                                                                                                                                                                                                                                                                                                                Batteries.RBMap α β cmpα × β

                                                                                                                                                                                                                                                                                                                                                O(log n). Returns the minimum element of the map, or panics if the map is empty.

                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                • Batteries.RBMap.min! = Batteries.RBSet.min!
                                                                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                                                                  @[inline]
                                                                                                                                                                                                                                                                                                                                                  def Batteries.RBMap.max! {α : Type u} {β : Type v} {cmp : ααOrdering} [Inhabited α] [Inhabited β] :
                                                                                                                                                                                                                                                                                                                                                  Batteries.RBMap α β cmpα × β

                                                                                                                                                                                                                                                                                                                                                  O(log n). Returns the maximum element of the map, or panics if the map is empty.

                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                  • Batteries.RBMap.max! = Batteries.RBSet.max!
                                                                                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                                                                                    @[inline]
                                                                                                                                                                                                                                                                                                                                                    def Batteries.RBMap.find! {α : Type u} {β : Type v} {cmp : ααOrdering} [Inhabited β] (t : Batteries.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 = (t.find? k).getD (panicWithPosWithDecl "Batteries.Data.RBMap.Basic" "Batteries.RBMap.find!" 1131 20 "key is not in the map")
                                                                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                                                                      def Batteries.RBMap.mergeWith {α : Type u} {β : Type v} {cmp : ααOrdering} (mergeFn : αβββ) (t₁ : Batteries.RBMap α β cmp) (t₂ : Batteries.RBMap α β cmp) :
                                                                                                                                                                                                                                                                                                                                                      Batteries.RBMap α β cmp

                                                                                                                                                                                                                                                                                                                                                      O(n₂ * log (n₁ + n₂)). 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 Batteries.RBMap.intersectWith {α : Type u} {β : Type v} {cmp : ααOrdering} {γ : Type u_1} {δ : Type u_2} (mergeFn : αβγδ) (t₁ : Batteries.RBMap α β cmp) (t₂ : Batteries.RBMap α γ cmp) :
                                                                                                                                                                                                                                                                                                                                                        Batteries.RBMap α δ cmp

                                                                                                                                                                                                                                                                                                                                                        O(n₁ * log (n₁ + n₂)). Intersects the maps t₁ and t₂ using mergeFn a b to produce the new value.

                                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                                                                                          def Batteries.RBMap.filter {α : Type u} {β : Type v} {cmp : ααOrdering} (t : Batteries.RBMap α β cmp) (p : αβBool) :
                                                                                                                                                                                                                                                                                                                                                          Batteries.RBMap α β cmp

                                                                                                                                                                                                                                                                                                                                                          O(n * log n). Constructs the set of all elements satisfying p.

                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                                                                                                                            def Batteries.RBMap.sdiff {α : Type u} {β : Type v} {cmp : ααOrdering} (t₁ : Batteries.RBMap α β cmp) (t₂ : Batteries.RBMap α β cmp) :
                                                                                                                                                                                                                                                                                                                                                            Batteries.RBMap α β cmp

                                                                                                                                                                                                                                                                                                                                                            O(n₁ * (log n₁ + log n₂)). Constructs the set of all elements of t₁ that are not in t₂.

                                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                                            • t₁.sdiff t₂ = t₁.filter fun (a : α) (x : β) => !t₂.contains a
                                                                                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                                                                                              @[reducible, inline]
                                                                                                                                                                                                                                                                                                                                                              abbrev List.toRBMap {α : Type u_1} {β : Type u_2} (l : List (α × β)) (cmp : ααOrdering) :
                                                                                                                                                                                                                                                                                                                                                              Batteries.RBMap α β cmp

                                                                                                                                                                                                                                                                                                                                                              O(n log n). Build a tree from an unsorted list by inserting them one at a time.

                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                              Instances For