Documentation

Init.Data.Array.Subarray

structure Subarray (α : Type u) :
  • array : Array α
  • start : Nat
  • stop : Nat
  • start_le_stop : self.start self.stop
  • stop_le_array_size : self.stop self.array.size
Instances For
    theorem Subarray.start_le_stop {α : Type u} (self : Subarray α) :
    self.start self.stop
    theorem Subarray.stop_le_array_size {α : Type u} (self : Subarray α) :
    self.stop self.array.size
    @[reducible, inline, deprecated Subarray.array]
    abbrev Subarray.as {α : Type u_1} (s : Subarray α) :
    Equations
    • s.as = s.array
    Instances For
      @[deprecated Subarray.start_le_stop]
      theorem Subarray.h₁ {α : Type u_1} (s : Subarray α) :
      s.start s.stop
      @[deprecated Subarray.stop_le_array_size]
      theorem Subarray.h₂ {α : Type u_1} (s : Subarray α) :
      s.stop s.array.size
      def Subarray.size {α : Type u_1} (s : Subarray α) :
      Equations
      • s.size = s.stop - s.start
      Instances For
        theorem Subarray.size_le_array_size {α : Type u_1} {s : Subarray α} :
        s.size s.array.size
        def Subarray.get {α : Type u_1} (s : Subarray α) (i : Fin s.size) :
        α
        Equations
        • s.get i = s.array[s.start + i]
        Instances For
          instance Subarray.instGetElemNatLtSize {α : Type u_1} :
          GetElem (Subarray α) Nat α fun (xs : Subarray α) (i : Nat) => i < xs.size
          Equations
          • Subarray.instGetElemNatLtSize = { getElem := fun (xs : Subarray α) (i : Nat) (h : i < xs.size) => xs.get i, h }
          @[inline]
          def Subarray.getD {α : Type u_1} (s : Subarray α) (i : Nat) (v₀ : α) :
          α
          Equations
          • s.getD i v₀ = if h : i < s.size then s.get i, h else v₀
          Instances For
            @[reducible, inline]
            abbrev Subarray.get! {α : Type u_1} [Inhabited α] (s : Subarray α) (i : Nat) :
            α
            Equations
            • s.get! i = s.getD i default
            Instances For
              def Subarray.popFront {α : Type u_1} (s : Subarray α) :
              Equations
              • s.popFront = if h : s.start < s.stop then { array := s.array, start := s.start + 1, stop := s.stop, start_le_stop := , stop_le_array_size := } else s
              Instances For
                def Subarray.empty {α : Type u_1} :

                The empty subarray.

                Equations
                Instances For
                  Equations
                  • Subarray.instEmptyCollection = { emptyCollection := Subarray.empty }
                  instance Subarray.instInhabited {α : Type u_1} :
                  Equations
                  • Subarray.instInhabited = { default := }
                  @[inline]
                  unsafe def Subarray.forInUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (s : Subarray α) (b : β) (f : αβm (ForInStep β)) :
                  m β
                  Instances For
                    @[specialize #[]]
                    unsafe def Subarray.forInUnsafe.loop {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (s : Subarray α) (f : αβm (ForInStep β)) (sz : USize) (i : USize) (b : β) :
                    m β
                    Instances For
                      @[implemented_by Subarray.forInUnsafe]
                      opaque Subarray.forIn {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (s : Subarray α) (b : β) (f : αβm (ForInStep β)) :
                      m β
                      instance Subarray.instForIn {m : Type u_1 → Type u_2} {α : Type u_3} :
                      ForIn m (Subarray α) α
                      Equations
                      • Subarray.instForIn = { forIn := fun {β : Type ?u.20} [Monad m] => Subarray.forIn }
                      @[inline]
                      def Subarray.foldlM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : βαm β) (init : β) (as : Subarray α) :
                      m β
                      Equations
                      Instances For
                        @[inline]
                        def Subarray.foldrM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : αβm β) (init : β) (as : Subarray α) :
                        m β
                        Equations
                        Instances For
                          @[inline]
                          def Subarray.anyM {α : Type u} {m : TypeType w} [Monad m] (p : αm Bool) (as : Subarray α) :
                          Equations
                          Instances For
                            @[inline]
                            def Subarray.allM {α : Type u} {m : TypeType w} [Monad m] (p : αm Bool) (as : Subarray α) :
                            Equations
                            Instances For
                              @[inline]
                              def Subarray.forM {α : Type u} {m : Type v → Type w} [Monad m] (f : αm PUnit) (as : Subarray α) :
                              Equations
                              Instances For
                                @[inline]
                                def Subarray.forRevM {α : Type u} {m : Type v → Type w} [Monad m] (f : αm PUnit) (as : Subarray α) :
                                Equations
                                Instances For
                                  @[inline]
                                  def Subarray.foldl {α : Type u} {β : Type v} (f : βαβ) (init : β) (as : Subarray α) :
                                  β
                                  Equations
                                  Instances For
                                    @[inline]
                                    def Subarray.foldr {α : Type u} {β : Type v} (f : αββ) (init : β) (as : Subarray α) :
                                    β
                                    Equations
                                    Instances For
                                      @[inline]
                                      def Subarray.any {α : Type u} (p : αBool) (as : Subarray α) :
                                      Equations
                                      Instances For
                                        @[inline]
                                        def Subarray.all {α : Type u} (p : αBool) (as : Subarray α) :
                                        Equations
                                        Instances For
                                          @[inline]
                                          def Subarray.findSomeRevM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Subarray α) (f : αm (Option β)) :
                                          m (Option β)
                                          Equations
                                          Instances For
                                            @[specialize #[]]
                                            def Subarray.findSomeRevM?.find {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Subarray α) (f : αm (Option β)) (i : Nat) :
                                            i as.sizem (Option β)
                                            Equations
                                            Instances For
                                              @[inline]
                                              def Subarray.findRevM? {α : Type} {m : TypeType w} [Monad m] (as : Subarray α) (p : αm Bool) :
                                              m (Option α)
                                              Equations
                                              • as.findRevM? p = as.findSomeRevM? fun (a : α) => do let __do_liftp a pure (if __do_lift = true then some a else none)
                                              Instances For
                                                @[inline]
                                                def Subarray.findRev? {α : Type} (as : Subarray α) (p : αBool) :
                                                Equations
                                                • as.findRev? p = (as.findRevM? p).run
                                                Instances For
                                                  def Array.toSubarray {α : Type u} (as : Array α) (start : optParam Nat 0) (stop : optParam Nat as.size) :
                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    def Array.ofSubarray {α : Type u} (s : Subarray α) :
                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      instance Array.instCoeSubarray {α : Type u} :
                                                      Coe (Subarray α) (Array α)
                                                      Equations
                                                      • Array.instCoeSubarray = { coe := Array.ofSubarray }
                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        Instances For
                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For
                                                            def Subarray.toArray {α : Type u_1} (s : Subarray α) :
                                                            Equations
                                                            • s.toArray = s
                                                            Instances For
                                                              instance instAppendSubarray {α : Type u_1} :
                                                              Equations
                                                              • instAppendSubarray = { append := fun (x y : Subarray α) => let a := x.toArray ++ y.toArray; a.toSubarray }
                                                              instance instReprSubarray {α : Type u_1} [Repr α] :
                                                              Equations
                                                              instance instToStringSubarray {α : Type u_1} [ToString α] :
                                                              Equations