feat: order the output of #print axioms (leanprover#4416)

Closes leanprover#4415
opencompl · Jun 10, 2024 · 366f3ac · 366f3ac
1 parent ea46bf2
commit 366f3ac
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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