mathlib documentation

core / init.data.array.slice

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, _⟩
def array.take {α : Type u} {n : } (a : array n α) (m : ) (h : m n) :
array m α

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

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

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

Equations