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} :
    Lake.RBArray α β cmp
    Equations
    • Lake.RBArray.empty = { toRBMap := Lean.RBMap.empty, toArray := #[] }
    Instances For
      instance Lake.RBArray.instEmptyCollection {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} :
      Equations
      • Lake.RBArray.instEmptyCollection = { emptyCollection := Lake.RBArray.empty }
      def Lake.RBArray.mkEmpty {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} (size : Nat) :
      Lake.RBArray α β cmp
      Equations
      Instances For
        @[inline]
        def Lake.RBArray.find? {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} (self : Lake.RBArray α β cmp) (a : α) :
        Equations
        • self.find? a = self.toRBMap.find? a
        Instances For
          @[inline]
          def Lake.RBArray.contains {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} (self : Lake.RBArray α β cmp) (a : α) :
          Equations
          • self.contains a = self.toRBMap.contains a
          Instances For
            def Lake.RBArray.insert {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} (self : Lake.RBArray α β cmp) (a : α) (b : β) :
            Lake.RBArray α β cmp

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

            Equations
            • self.insert a b = if self.toRBMap.contains a = true then self else { toRBMap := self.toRBMap.insert a b, toArray := self.toArray.push b }
            Instances For
              @[inline]
              def Lake.RBArray.all {β : Type u_1} {α : Type u_2} {cmp : ααOrdering} (f : βBool) (self : Lake.RBArray α β cmp) :
              Equations
              Instances For
                @[inline]
                def Lake.RBArray.any {β : Type u_1} {α : Type u_2} {cmp : ααOrdering} (f : βBool) (self : Lake.RBArray α β cmp) :
                Equations
                Instances For
                  @[inline]
                  def Lake.RBArray.foldl {σ : Type u_1} {β : Type u_2} {α : Type u_3} {cmp : ααOrdering} (f : σβσ) (init : σ) (self : Lake.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 : Lake.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 : Lake.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 : Lake.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 : Lake.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 : Lake.RBArray α β cmp) (init : σ) (f : βσm (ForInStep σ)) :
                            m σ
                            Equations
                            • self.forIn init f = self.toArray.forIn init f
                            Instances For
                              instance Lake.RBArray.instForIn {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {cmp : ααOrdering} :
                              ForIn m (Lake.RBArray α β cmp) β
                              Equations
                              • Lake.RBArray.instForIn = { forIn := fun {β_1 : Type ?u.37} [Monad m] => Lake.RBArray.forIn }
                              @[inline]
                              def Lake.mkRBArray {β : Type u_1} {α : Type u_2} {cmp : ααOrdering} (f : βα) (vs : Array β) :
                              Lake.RBArray α β cmp
                              Equations
                              Instances For