Documentation
Init
.
Data
.
Array
.
QSort
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