HepLean Documentation
Init
.
Data
.
Array
.
QSort
Search
Google site search
return to top
source
Imports
Init.Data.Ord
Init.Data.Array.Basic
Imported by
Array
.
qpartition
Array
.
qpartition
.
loop
Array
.
qsort
Array
.
qsort
.
sort
Array
.
qsortOrd
source
def
Array
.
qpartition
{α :
Type
u_1}
(as :
Array
α
)
(lt :
α
→
α
→
Bool
)
(lo hi :
Nat
)
:
Nat
×
Array
α
Equations
One or more equations did not get rendered due to their size.
Instances For
source
@[irreducible]
def
Array
.
qpartition
.
loop
{α :
Type
u_1}
(lt :
α
→
α
→
Bool
)
(hi :
Nat
)
(this :
Inhabited
α
)
(pivot :
α
)
(as :
Array
α
)
(i 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 :
Nat
:=
0
)
(high :
Nat
:=
as
.size
-
1
)
:
Array
α
Equations
as
.qsort
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 high :
Nat
)
:
Array
α
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