chore: reduce churn in tests/lean/run/meta5.lean (#6480)

leanprover · Dec 31, 2024 · 32dc165 · 32dc165
1 parent 7e8e22e
commit 32dc165
Showing 1 changed file with 8 additions and 4 deletions.
diff --git a/tests/lean/run/meta5.lean b/tests/lean/run/meta5.lean
@@ -14,9 +14,13 @@ withLetDecl `x (mkConst `Nat) (mkNatLit 0) $ fun x => do {
   mvar.mvarId!.assign v;
   trace[Meta.debug] mvar;
   trace[Meta.debug] r;
+
   let mctx ← getMCtx;
-  mctx.decls.forM fun mvarId mvarDecl => do
-    trace[Meta.debug] m!"?{mvarId.name} : {mvarDecl.type}"
+  let sortedDecls := mctx.decls.toArray.qsort (fun ⟨v1, _⟩ ⟨v2, _⟩ => v1.name.lt v2.name);
+  let mut i : Nat := 0;
+  for ⟨_, mvarDecl⟩ in sortedDecls do
+    trace[Meta.debug] m!"?{i} : {mvarDecl.type}";
+    i := i + 1;
 }
 
 set_option pp.mvars false
@@ -31,8 +35,8 @@ info: [Meta.debug] ?_
 [Meta.debug] fun y =>
       let x := 0;
       x.add y
-[Meta.debug] ?_uniq.3037 : Nat
-[Meta.debug] ?_uniq.3038 : Nat → Nat → Nat
+[Meta.debug] ?0 : Nat
+[Meta.debug] ?1 : Nat → Nat → Nat
 -/
 #guard_msgs in
 #eval tst1