Documentation
Init
.
Data
.
Array
.
QSort
Search
Google site search
return to top
source
Imports
Init.Data.Array.Basic
Imported by
Array
.
qpartition
Array
.
qpartition
.
loop
Array
.
qsort
Array
.
qsort
.
sort
source
def
Array
.
qpartition
{α :
Type
u_1}
(as :
Array
α
)
(lt :
α
→
α
→
Bool
)
(lo :
Nat
)
(hi :
Nat
)
:
Nat
×
Array
α
Equations
One or more equations did not get rendered due to their size.
Instances For
source
def
Array
.
qpartition
.
loop
{α :
Type
u_1}
(lt :
α
→
α
→
Bool
)
(hi :
Nat
)
(this :
Inhabited
α
)
(pivot :
α
)
(as :
Array
α
)
(i :
Nat
)
(j :
Nat
)
:
Nat
×
Array
α
Equations
One or more equations did not get rendered due to their size.
Instances For
source
@[inline]
def
Array
.
qsort
{α :
Type
u_1}
(as :
Array
α
)
(lt :
α
→
α
→
Bool
)
(low :
optParam
Nat
0
)
(high :
optParam
Nat
(
Array.size
as
-
1
)
)
:
Array
α
Equations
Array.qsort
as
lt
low
high
=
Array.qsort.sort
lt
as
low
high
Instances For
source
@[specialize #[]]
partial def
Array
.
qsort
.
sort
{α :
Type
u_1}
(lt :
α
→
α
→
Bool
)
(as :
Array
α
)
(low :
Nat
)
(high :
Nat
)
:
Array
α