From 3bd01de3840ad05ebfa99ccef9fc5586a3417b15 Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Sun, 29 Sep 2024 15:50:25 +1000
Subject: [PATCH] feat: upstream Array.qsortOrd (#5515)

---
 src/Init/Data/Array/QSort.lean | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/src/Init/Data/Array/QSort.lean b/src/Init/Data/Array/QSort.lean
index 1f71a07bb4..9f2e8c29b7 100644
--- a/src/Init/Data/Array/QSort.lean
+++ b/src/Init/Data/Array/QSort.lean
@@ -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