From 366f3ac272b6a12b19cabd8573652fc138804bdf Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Mon, 10 Jun 2024 11:17:05 +0200
Subject: [PATCH] feat: order the output of #print axioms (#4416)

Closes #4415
---
 src/Lean/Elab/Print.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Elab/Print.lean b/src/Lean/Elab/Print.lean
index e12e995c3f77..2e1a81680f41 100644
--- a/src/Lean/Elab/Print.lean
+++ b/src/Lean/Elab/Print.lean
@@ -153,7 +153,7 @@ private def printAxiomsOf (constName : Name) : CommandElabM Unit := do
   if s.axioms.isEmpty then
     logInfo m!"'{constName}' does not depend on any axioms"
   else
-    logInfo m!"'{constName}' depends on axioms: {s.axioms.toList}"
+    logInfo m!"'{constName}' depends on axioms: {s.axioms.qsort Name.lt |>.toList}"
 
 @[builtin_command_elab «printAxioms»] def elabPrintAxioms : CommandElab
   | `(#print%$tk axioms $id) => withRef tk do