Init.Data.Array.BinSearch

@[specialize]

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

Nat → Nat → β

source

@[inline]

def Array.binSearch {α : Type} [inst : Inhabited α] (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

source

@[inline]

def Array.binSearchContains {α : Type} [inst : Inhabited α] (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.

source

@[specialize]

def Array.binInsertM {α : Type u} {m : Type u → Type v} [inst : Monad m] [inst : Inhabited α] (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.

source

@[inline]

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

Array α

Equations

Array.binInsert lt as k = Id.run (Array.binInsertM lt (fun x => k) (fun x => k) as k)