source
@[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.

Instances For

source
@[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.

Instances For

source
@[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.

Instances For

source
@[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.

Instances For

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

Instances For