Documentation
Init
.
Data
.
Array
.
QSort
Search
Google site search
return to top
source
Imports
Init.Data.Ord
Init.Data.Vector.Basic
Imported by
Array
.
qsort
Array
.
qsort
.
sort
Array
.
qsortOrd
source
@[inline]
def
Array
.
qsort
{α :
Type
u_1}
(as :
Array
α
)
(lt :
α
→
α
→
Bool
:= by exact (· < ·))
(low :
Nat
:=
0
)
(high :
Nat
:=
as
.size
-
1
)
:
Array
α
Equations
One or more equations did not get rendered due to their size.
Instances For
source
@[irreducible, specialize #[]]
def
Array
.
qsort
.
sort
{α :
Type
u_1}
(lt :
α
→
α
→
Bool
:= by exact (· < ·))
{n :
Nat
}
(as :
Vector
α
n
)
(lo hi :
Nat
)
(hlo :
lo
<
n
:= by omega)
(hhi :
hi
<
n
:= by omega)
:
Vector
α
n
Equations
One or more equations did not get rendered due to their size.
Instances For
source
def
Array
.
qsortOrd
{α :
Type
u_1}
[ord :
Ord
α
]
(xs :
Array
α
)
:
Array
α
Sort an array using
compare
to compare elements.
Equations
xs
.qsortOrd
=
xs
.qsort
fun (
x
y
:
α
) =>
(
compare
x
y
)
.isLT
Instances For