Documentation

Lake.Util.RBArray

structure Lake.RBArray (α : Type u) (β : Type v) (cmp : ααOrdering) :
Type (max u v)

There are two ways to think of this type:

  • As an Array of values with an RBMap key-value index for the key α.
  • As an RBMap that preserves insertion order, but is optimized for iteration-by-values. Thus, it does not store the order of keys.
Instances For
    def Lake.RBArray.empty {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} :
    RBArray α β cmp
    Equations
      Instances For
        instance Lake.RBArray.instEmptyCollection {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} :
        Equations
          def Lake.RBArray.mkEmpty {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} (size : Nat) :
          RBArray α β cmp
          Equations
            Instances For
              @[inline]
              def Lake.RBArray.find? {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} (self : RBArray α β cmp) (a : α) :
              Equations
                Instances For
                  @[inline]
                  def Lake.RBArray.contains {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} (self : RBArray α β cmp) (a : α) :
                  Equations
                    Instances For
                      def Lake.RBArray.insert {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} (self : RBArray α β cmp) (a : α) (b : β) :
                      RBArray α β cmp

                      Insert b with the key a. Does nothing if the key is already present.

                      Equations
                        Instances For
                          @[inline]
                          def Lake.RBArray.all {β : Type u_1} {α : Type u_2} {cmp : ααOrdering} (f : βBool) (self : RBArray α β cmp) :
                          Equations
                            Instances For
                              @[inline]
                              def Lake.RBArray.any {β : Type u_1} {α : Type u_2} {cmp : ααOrdering} (f : βBool) (self : RBArray α β cmp) :
                              Equations
                                Instances For
                                  @[inline]
                                  def Lake.RBArray.foldl {σ : Type u_1} {β : Type u_2} {α : Type u_3} {cmp : ααOrdering} (f : σβσ) (init : σ) (self : RBArray α β cmp) :
                                  σ
                                  Equations
                                    Instances For
                                      @[inline]
                                      def Lake.RBArray.foldlM {m : Type u_1 → Type u_2} {σ : Type u_1} {β : Type u_3} {α : Type u_4} {cmp : ααOrdering} [Monad m] (f : σβm σ) (init : σ) (self : RBArray α β cmp) :
                                      m σ
                                      Equations
                                        Instances For
                                          @[inline]
                                          def Lake.RBArray.foldr {β : Type u_1} {σ : Type u_2} {α : Type u_3} {cmp : ααOrdering} (f : βσσ) (init : σ) (self : RBArray α β cmp) :
                                          σ
                                          Equations
                                            Instances For
                                              @[inline]
                                              def Lake.RBArray.foldrM {m : Type u_1 → Type u_2} {β : Type u_3} {σ : Type u_1} {α : Type u_4} {cmp : ααOrdering} [Monad m] (f : βσm σ) (init : σ) (self : RBArray α β cmp) :
                                              m σ
                                              Equations
                                                Instances For
                                                  @[inline]
                                                  def Lake.RBArray.forM {m : Type u_1 → Type u_2} {β : Type u_3} {α : Type u_4} {cmp : ααOrdering} [Monad m] (f : βm PUnit) (self : RBArray α β cmp) :
                                                  Equations
                                                    Instances For
                                                      @[inline]
                                                      def Lake.RBArray.forIn {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {cmp : ααOrdering} {σ : Type u_1} [Monad m] (self : RBArray α β cmp) (init : σ) (f : βσm (ForInStep σ)) :
                                                      m σ
                                                      Equations
                                                        Instances For
                                                          instance Lake.RBArray.instForIn {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {cmp : ααOrdering} :
                                                          ForIn m (RBArray α β cmp) β
                                                          Equations
                                                            @[inline]
                                                            def Lake.mkRBArray {β : Type u_1} {α : Type u_2} {cmp : ααOrdering} (f : βα) (vs : Array β) :
                                                            RBArray α β cmp
                                                            Equations
                                                              Instances For