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

@[inline]

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

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

@[inline]

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