@[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 → β

@[inline]

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

Binary search for an element equivalent to k in the sorted array as. Returns the element from the array, if it is found, or none otherwise.

The array as must be sorted according to the comparison operator lt, which should be a total order.

The optional parameters lo and hi determine the region of the array indices to be searched. Both are inclusive, and default to searching the entire array.

@[inline]

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

Binary search for an element equivalent to k in the sorted array as. Returns true if the element is found, or false otherwise.

The array as must be sorted according to the comparison operator lt, which should be a total order.

The optional parameters lo and hi determine the region of the array indices to be searched. Both are inclusive, and default to searching the entire array.

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

Inserts an element k into a sorted array as such that the resulting array is sorted.

The ordering predicate lt should be a total order on elements, and the array as should be sorted with respect to lt.

If an element that lt equates to k is already present in as, then merge is applied to the existing element to determine the value of that position in the resulting array. If no element equal to k is present, then add is used to determine the value to be inserted.

@[inline]

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

Inserts an element into a sorted array such that the resulting array is sorted. If the element is already present in the array, it is not inserted.

The ordering predicate lt should be a total order on elements, and the array as should be sorted with respect to lt.

Array.binInsertM is a more general operator that provides greater control over the handling of duplicate elements in addition to running in a monad.

Examples:

• #[0, 1, 3, 5].binInsert (· < ·) 2 = #[0, 1, 2, 3, 5]
• #[0, 1, 3, 5].binInsert (· < ·) 1 = #[0, 1, 3, 5]
• #[].binInsert (· < ·) 1 = #[1]