Documentation

Init.Data.Array.BinSearch

@[specialize]
partial def Array.binSearchAux {α : Type u} {β : Type v} [inst : Inhabited α] [inst : Inhabited β] (lt : ααBool) (found : Option αβ) (as : Array α) (k : α) :
NatNatβ
@[inline]
def Array.binSearch {α : Type} [inst : Inhabited α] (as : Array α) (k : α) (lt : ααBool) (lo : optParam Nat 0) (hi : optParam Nat (Array.size as - 1)) :
Equations
@[inline]
def Array.binSearchContains {α : Type} [inst : Inhabited α] (as : Array α) (k : α) (lt : ααBool) (lo : optParam Nat 0) (hi : optParam Nat (Array.size as - 1)) :
Equations
@[specialize]
def Array.binInsertM {α : Type u} {m : Type uType v} [inst : Monad m] [inst : Inhabited α] (lt : ααBool) (merge : αm α) (add : Unitm α) (as : Array α) (k : α) :
m (Array α)
Equations
@[inline]
def Array.binInsert {α : Type u} [inst : Inhabited α] (lt : ααBool) (as : Array α) (k : α) :
Equations