def Array.head? {α : Type u_1} (a : Array α) : Option (α × Array α)

get head element and array without head element

Equations

• a.head? = match a.data with | [] => none | head :: tail => some (head, { data := tail })

def Array.pop? {α : Type u_1} (a : Array α) : Option (α × Array α)

get last element and array without last element

Equations

• a.pop? = if h : 0 < a.data.length then some (a.data.get ⟨a.data.length - 1, ⋯⟩, a.pop) else none

def Array.last? {α : Type u_1} (a : Array α) : Option α

get last element of array

Equations

• a.last? = if h : 0 < a.data.length then some (a.data.get ⟨a.data.length - 1, ⋯⟩) else none

def Array.unique {α : Type u_1} [BEq α] (intervals : Array α) : Array α

unique array of sorted array

Equations

• One or more equations did not get rendered due to their size.