feat: upstream Array.qsortOrd (#5515)

This commit is contained in:
Kim Morrison 2024-09-29 15:50:25 +10:00 committed by GitHub
parent 8835ab46ad
commit 3bd01de384
No known key found for this signature in database
GPG key ID: B5690EEEBB952194

View file

@ -5,6 +5,7 @@ Authors: Leonardo de Moura
-/
prelude
import Init.Data.Array.Basic
import Init.Data.Ord
namespace Array
-- TODO: remove the [Inhabited α] parameters as soon as we have the tactic framework for automating proof generation and using Array.fget
@ -44,4 +45,11 @@ def qpartition (as : Array α) (lt : αα → Bool) (lo hi : Nat) : Nat ×
else as
sort as low high
set_option linter.unusedVariables.funArgs false in
/--
Sort an array using `compare` to compare elements.
-/
def qsortOrd [ord : Ord α] (xs : Array α) : Array α :=
xs.qsort fun x y => compare x y |>.isLT
end Array