Documentation

Init.Data.Array.Subarray

structure Subarray (α : Type u) :
Instances For
    def Subarray.size {α : Type u_1} (s : Subarray α) :
    Equations
    Instances For
      def Subarray.get {α : Type u_1} (s : Subarray α) (i : Fin (Subarray.size s)) :
      α
      Equations
      Instances For
        Equations
        • Subarray.instGetElemSubarrayNatLtInstLTNatSize = { getElem := fun xs i h => Subarray.get xs { val := i, isLt := h } }
        @[inline]
        def Subarray.getD {α : Type u_1} (s : Subarray α) (i : Nat) (v₀ : α) :
        α
        Equations
        Instances For
          @[inline, reducible]
          abbrev Subarray.get! {α : Type u_1} [Inhabited α] (s : Subarray α) (i : Nat) :
          α
          Equations
          Instances For
            def Subarray.popFront {α : Type u_1} (s : Subarray α) :
            Equations
            • Subarray.popFront s = if h : s.start < s.stop then { as := s.as, start := s.start + 1, stop := s.stop, h₁ := (_ : s.start + 1 s.stop), h₂ := (_ : s.stop Array.size s.as) } else s
            Instances For
              @[inline]
              unsafe def Subarray.forInUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (s : Subarray α) (b : β) (f : αβm (ForInStep β)) :
              m β
              Equations
              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 β
                Equations
                • One or more equations did not get rendered due to their size.
                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.instForInSubarray {m : Type u_1 → Type u_2} {α : Type u_3} :
                  ForIn m (Subarray α) α
                  Equations
                  • Subarray.instForInSubarray = { forIn := fun {β} [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 Subarray.size asm (Option β)
                                        Equations
                                        Instances For
                                          @[inline]
                                          def Subarray.findRevM? {α : Type} {m : TypeType w} [Monad m] (as : Subarray α) (p : αm Bool) :
                                          m (Option α)
                                          Equations
                                          Instances For
                                            @[inline]
                                            def Subarray.findRev? {α : Type} (as : Subarray α) (p : αBool) :
                                            Equations
                                            Instances For
                                              def Array.toSubarray {α : Type u} (as : Array α) (start : optParam Nat 0) (stop : optParam Nat (Array.size as)) :
                                              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.instCoeSubarrayArray {α : Type u} :
                                                  Coe (Subarray α) (Array α)
                                                  Equations
                                                  • Array.instCoeSubarrayArray = { 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
                                                        Instances For
                                                          instance instAppendSubarray {α : Type u_1} :
                                                          Equations
                                                          instance instReprSubarray {α : Type u_1} [Repr α] :
                                                          Equations
                                                          instance instToStringSubarray {α : Type u_1} [ToString α] :
                                                          Equations