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} [DecidableEq α] (as : Array α) : Array α

unique array of sorted array

Equations

• as.unique = match as.toList with | [] => #[] | [r] => #[r] | head :: tail => (List.foldl Array.unique.acc (head, #[head]) tail).snd

def Array.unique.acc {α : Type u_1} [DecidableEq α] (x : α × Array α) (r : α) : α × Array α

Equations

• Array.unique.acc x r = if x.fst = r then (r, x.snd) else (r, x.snd.push r)

def Array.mergeSort {α : Type u_1} (as : Array α) (le : α → α → Bool := by exact fun a b => a ≤ b) : Array α

Equations

• as.mergeSort le = (as.toList.mergeSort le).toArray

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