@[irreducible, specialize #[]]

def Array.binSearchAux {α : Type u} {β : Type v} (lt : α → α → Bool) (found : Option α → β) (as : Array α) (k : α) (lo : Fin (as.size + 1)) (hi : Fin as.size) : ↑lo ≤ ↑hi → β

@[inline]

def Array.binSearch {α : Type} (as : Array α) (k : α) (lt : α → α → Bool) (lo : Nat := 0) (hi : Nat := as.size - 1) : Option α

Equations

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

@[inline]

def Array.binSearchContains {α : Type} (as : Array α) (k : α) (lt : α → α → Bool) (lo : Nat := 0) (hi : Nat := as.size - 1) : Bool

Equations

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

@[specialize #[]]

def Array.binInsertM {α : Type u} {m : Type u → Type v} [Monad m] (lt : α → α → Bool) (merge : α → m α) (add : Unit → m α) (as : Array α) (k : α) : m (Array α)

Equations

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

@[inline]

def Array.binInsert {α : Type u} (lt : α → α → Bool) (as : Array α) (k : α) : Array α

Equations

• Array.binInsert lt as k = (Array.binInsertM lt (fun (x : α) => k) (fun (x : Unit) => k) as k).run