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

get head element and array without head element

Equations

• a.head? = match a.toList with | [] => none | head :: tail => some (head, { toList := 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.toList.length then some (a.toList.get ⟨a.toList.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.toList.length then some (a.toList.get ⟨a.toList.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.

def Array.map_option_subtype {α : Type u_1} {p : α → Prop} [DecidablePred p] (arr : Array (Option { m : α // p m })) : { arr : Array (Option α) // (arr.all fun (x : Option α) => Option.all (fun (x : α) => decide (p x)) x) = true }

Unattach values of subtype in arr and collect their properties.

Equations

• arr.map_option_subtype = ⟨Array.map (Option.map fun (x : { m : α // p m }) => x.val) arr, ⋯⟩

def Array.all_contains {α : Type u_1} [BEq α] (as bs : Array α) : Bool

as.contains bs is true if as contains all elems of bs.

Equations

• as.all_contains bs = bs.all fun (b : α) => as.contains b