mathlib documentation

core.​init.​data.​array.​slice

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