Documentation
Miri
.
Memory
.
QSortProof
Search
return to top
source
Imports
Init
Init.Data.Array.QSort.Basic
Imported by
Miri
.
Memory
.
QSortProof
.
singleton
source
theorem
Miri
.
Memory
.
QSortProof
.
singleton
{
A
:
Type
}
(
value
:
A
)
(
less
:
A
→
A
→
Bool
)
:
#[
value
]
.
qsort
less
0
0
=
#[
value
]