Documentation
Init
.
Data
.
Array
.
InsertionSort
Search
return to top
source
Imports
Init.Data.Array.Basic
Imported by
Array
.
insertionSort
Array
.
insertionSort
.
traverse
Array
.
insertionSort
.
swapLoop
source
@[inline]
def
Array
.
insertionSort
{α :
Type
u_1}
(a :
Array
α
)
(lt :
α
→
α
→
Bool
:= by exact (· < ·))
:
Array
α
Equations
a
.
insertionSort
lt
=
Array.insertionSort.traverse
lt
a
0
a
.
size
Instances For
source
@[specialize #[]]
def
Array
.
insertionSort
.
traverse
{α :
Type
u_1}
(lt :
α
→
α
→
Bool
:= by exact (· < ·))
(a :
Array
α
)
(i fuel :
Nat
)
:
Array
α
Equations
Array.insertionSort.traverse
lt
a
i
0
=
a
Array.insertionSort.traverse
lt
a
i
fuel_2
.
succ
=
if h :
i
<
a
.
size
then
Array.insertionSort.traverse
lt
(
Array.insertionSort.swapLoop
lt
a
i
h
)
(
i
+
1
)
fuel_2
else
a
Instances For
source
@[specialize #[]]
def
Array
.
insertionSort
.
swapLoop
{α :
Type
u_1}
(lt :
α
→
α
→
Bool
:= by exact (· < ·))
(a :
Array
α
)
(j :
Nat
)
(h :
j
<
a
.
size
)
:
Array
α
Equations
Array.insertionSort.swapLoop
lt
a
0
h
=
a
Array.insertionSort.swapLoop
lt
a
j'
.
succ
h
=
if
lt
a
[
j'
.
succ
]
a
[
j'
]
=
true
then
Array.insertionSort.swapLoop
lt
(
a
.
swap
j'
.
succ
j'
h
⋯
)
j'
⋯
else
a
Instances For