Documentation
Init
.
Data
.
Array
.
BinSearch
Search
Google site search
Init
.
Data
.
Array
.
BinSearch
source
Imports
Init.Data.Array.Basic
Imported by
Array
.
binSearchAux
Array
.
binSearch
Array
.
binSearchContains
Array
.
binInsertM
Array
.
binInsert
source
@[specialize #[]]
partial def
Array
.
binSearchAux
{α :
Type
u}
{β :
Type
v}
[
Inhabited
β
]
(lt :
α
→
α
→
Bool
)
(found :
Option
α
→
β
)
(as :
Array
α
)
(k :
α
)
:
Nat
→
Nat
→
β
source
@[inline]
def
Array
.
binSearch
{α :
Type
}
(as :
Array
α
)
(k :
α
)
(lt :
α
→
α
→
Bool
)
(lo :
optParam
Nat
0
)
(hi :
optParam
Nat
(
Array.size
as
-
1
)
)
:
Option
α
Instances For
source
@[inline]
def
Array
.
binSearchContains
{α :
Type
}
(as :
Array
α
)
(k :
α
)
(lt :
α
→
α
→
Bool
)
(lo :
optParam
Nat
0
)
(hi :
optParam
Nat
(
Array.size
as
-
1
)
)
:
Bool
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
α
)
Instances For
source
@[inline]
def
Array
.
binInsert
{α :
Type
u}
(lt :
α
→
α
→
Bool
)
(as :
Array
α
)
(k :
α
)
:
Array
α
Instances For