From bc17d4ca47cbdb62134b102dada65cc80c79bd94 Mon Sep 17 00:00:00 2001
From: lyphyser <lyphyser@gmail.com>
Date: Wed, 18 Sep 2024 09:59:15 +0000
Subject: [PATCH] Add doc comment for qsort

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

diff --git a/src/Init/Data/Array/QSort.lean b/src/Init/Data/Array/QSort.lean
index eb8da909aefe..e9b910e6807d 100644
--- a/src/Init/Data/Array/QSort.lean
+++ b/src/Init/Data/Array/QSort.lean
@@ -12,6 +12,13 @@ import Init.Data.Nat.Mod
 
 namespace Array
 
+/--
+Sorts the array using QuickSort according to function f.
+
+The function can be a ≤, a <, or in fact an arbitrary function (with weaker guarantees).
+
+See [qsort_sorts_of_is_le], [qsort_sorts_of_is_lt], [qsort_sorts], [qsort_sorts_as] for proofs.
+--/
 @[inline] def qsort (as : Array α) (f: α → α → Bool) (low := 0) (high := as.size - 1) : Array α :=
   let rec @[specialize] sort (as : Array α) (low high : Nat)
       (hhs: low < high → high < as.size): {as': Array α // as'.size = as.size} :=