@[specialize #[]]

partial def Array.binSearchAux {α : Type u} {β : Type v} [Inhabited β] (lt : α → α → Bool) (found : Option α → β) (as : Array α) (k : α) : Nat → Nat → β

@[inline]

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

Equations

• as.binSearch k lt lo hi = if lo < as.size then let hi := if hi < as.size then hi else as.size - 1; Array.binSearchAux lt id as k lo hi else none

@[inline]

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

Equations

• as.binSearchContains k lt lo hi = if lo < as.size then let hi := if hi < as.size then hi else as.size - 1; Array.binSearchAux lt Option.isSome as k lo hi else false

@[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