Documentation

Init.Data.Array.BinSearch

@[specialize #[]]
partial def Array.binSearchAux {α : Type u} {β : Type v} [Inhabited β] (lt : ααBool) (found : Option αβ) (as : Array α) (k : α) :
NatNatβ
@[inline]
def Array.binSearch {α : Type} (as : Array α) (k : α) (lt : ααBool) (lo : optParam Nat 0) (hi : optParam Nat (Array.size as - 1)) :
Equations
Instances For
    @[inline]
    def Array.binSearchContains {α : Type} (as : Array α) (k : α) (lt : ααBool) (lo : optParam Nat 0) (hi : optParam Nat (Array.size as - 1)) :
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[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.
      Instances For
        @[inline]
        def Array.binInsert {α : Type u} (lt : ααBool) (as : Array α) (k : α) :
        Equations
        Instances For