Documentation

Init.Data.Array.BinSearch

@[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β
Equations
  • One or more equations did not get rendered due to their size.
@[inline]
def Array.binSearch {α : Type} (as : Array α) (k : α) (lt : ααBool) (lo : Nat := 0) (hi : Nat := as.size - 1) :
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) :
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 : Unitm α) (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 : α) :
Equations