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