@[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) : 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.

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) : 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.

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 : 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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Array.binInsert lt as k = (Array.binInsertM lt (fun (x : α) => pure k) (fun (x : Unit) => pure k) as k).run