Init.Data.Array.Subarray

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

source

@[inline]

unsafe def Subarray.forInUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (s : Subarray α) (b : β) (f : α → β → m (ForInStep β)) :

m β

Equations

Subarray.forInUnsafe s b f = let sz := USize.ofNat s.stop; Subarray.forInUnsafe.loop s f sz (USize.ofNat s.start) b

source

@[specialize]

unsafe def Subarray.forInUnsafe.loop {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (s : Subarray α) (f : α → β → m (ForInStep β)) (sz : USize) (i : USize) (b : β) :

m β

Equations

Subarray.forInUnsafe.loop s f sz i b = if i < sz then let a := Array.uget s.as i (_ : USize.toNat i < Array.size s.as); do let a ← f a b match a with | ForInStep.done b => pure b | ForInStep.yield b => Subarray.forInUnsafe.loop s f sz (i + 1) b else pure b

source

@[implementedBy Subarray.forInUnsafe]

constant Subarray.forIn {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (s : Subarray α) (b : β) (f : α → β → m (ForInStep β)) :

m β

source

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 }

source

@[inline]

def Subarray.foldlM {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (f : β → α → m β) (init : β) (as : Subarray α) :

m β

Equations

Subarray.foldlM f init as = Array.foldlM f init as.as as.start as.stop

source

@[inline]

def Subarray.foldrM {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (f : α → β → m β) (init : β) (as : Subarray α) :

m β

Equations

Subarray.foldrM f init as = Array.foldrM f init as.as as.stop as.start

source

@[inline]

def Subarray.anyM {α : Type u} {m : Type → Type w} [inst : Monad m] (p : α → m Bool) (as : Subarray α) :

m Bool

Equations

Subarray.anyM p as = Array.anyM p as.as as.start as.stop

source

@[inline]

def Subarray.allM {α : Type u} {m : Type → Type w} [inst : Monad m] (p : α → m Bool) (as : Subarray α) :

m Bool

Equations

Subarray.allM p as = Array.allM p as.as as.start as.stop

source

@[inline]

def Subarray.forM {α : Type u} {m : Type v → Type w} [inst : Monad m] (f : α → m PUnit) (as : Subarray α) :

m PUnit

Equations

Subarray.forM f as = Array.forM f as.as as.start as.stop

source

@[inline]

def Subarray.forRevM {α : Type u} {m : Type v → Type w} [inst : Monad m] (f : α → m PUnit) (as : Subarray α) :

m PUnit

Equations

Subarray.forRevM f as = Array.forRevM f as.as as.stop as.start

source

@[inline]

def Subarray.foldl {α : Type u} {β : Type v} (f : β → α → β) (init : β) (as : Subarray α) :

β

Equations

Subarray.foldl f init as = Id.run (Subarray.foldlM f init as)

source

@[inline]

def Subarray.foldr {α : Type u} {β : Type v} (f : α → β → β) (init : β) (as : Subarray α) :

β

Equations

Subarray.foldr f init as = Id.run (Subarray.foldrM f init as)

source

@[inline]

def Subarray.any {α : Type u} (p : α → Bool) (as : Subarray α) :

Bool

Equations

Subarray.any p as = Id.run (Subarray.anyM p as)

source

@[inline]

def Subarray.all {α : Type u} (p : α → Bool) (as : Subarray α) :

Bool

Equations

Subarray.all p as = Id.run (Subarray.allM p as)

source

def Array.toSubarray {α : Type u} (as : Array α) (start : optParam Nat 0) (stop : optParam Nat (Array.size as)) :

Subarray α

Equations

Array.toSubarray as start stop = if h₂ : stop ≤ Array.size as then if h₁ : start ≤ stop then { as := as, start := start, stop := stop, h₁ := h₁, h₂ := h₂ } else { as := as, start := stop, stop := stop, h₁ := (_ : stop ≤ stop), h₂ := h₂ } else if h₁ : start ≤ Array.size as then { as := as, start := start, stop := Array.size as, h₁ := h₁, h₂ := (_ : Array.size as ≤ Array.size as) } else { as := as, start := Array.size as, stop := Array.size as, h₁ := (_ : Array.size as ≤ Array.size as), h₂ := (_ : Array.size as ≤ Array.size as) }