@[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 : optParam Nat 0) (hi : optParam Nat (Array.size as - 1)) : Option α

Equations

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

@[inline]

def Array.binSearchContains {α : Type} (as : Array α) (k : α) (lt : α → α → Bool) (lo : optParam Nat 0) (hi : optParam Nat (Array.size as - 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 = Id.run (Array.binInsertM lt (fun (x : α) => k) (fun (x : Unit) => k) as k)