mathlib documentation

core.init.data.array.slice

def array.slice {α : Type u} {n : } (a : array n α) (k l : ) :
k ll narray (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 : ) :
m narray m α

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

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

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

Equations