mathlib documentation

core.init.data.array.slice

source
def array.slice {α : Type u} {n : ℕ} (a : array n α) (k l : ℕ) (h₁ : k ≤ l) (h₂ : l ≤ n) :
array (l - k) α

Equations
  • a.slice k l h₁ h₂ = {data := λ (_x : fin (l - k)), array.slice._match_1 a k l h₁ h₂ _x}
  • array.slice._match_1 a k l h₁ h₂ ⟨i, hi⟩ = a.read ⟨i + k, _⟩
source
def array.take {α : Type u} {n : ℕ} (a : array n α) (m : ℕ) (h : m ≤ n) :
array m α

Equations
source
def array.drop {α : Type u} {n : ℕ} (a : array n α) (m : ℕ) (h : m ≤ n) :
array (n - m) α

Equations
source
def array.take_right {α : Type u} {n : ℕ} (a : array n α) (m : ℕ) (h : m ≤ n) :
array m α

Equations
source
def array.reverse {α : Type u} {n : ℕ} (a : array n α) :
array n α

Equations