chore: fix tests

leanprover · Nov 16, 2024 · 501f461 · 501f461
1 parent f4a3b9a
commit 501f461
Show file tree

Hide file tree

Showing 3 changed files with 16 additions and 14 deletions.
diff --git a/tests/lean/1018unknowMVarIssue.lean.expected.out b/tests/lean/1018unknowMVarIssue.lean.expected.out
@@ -56,8 +56,8 @@ a : α
           • Fam2.any : Fam2 α α @ ⟨9, 4⟩†-⟨9, 12⟩†
             • α : Type @ ⟨9, 4⟩†-⟨9, 12⟩†
           • a (isBinder := true) : α @ ⟨8, 2⟩†-⟨10, 19⟩†
-          • FVarAlias a: _uniq.585 -> _uniq.312
-          • FVarAlias α: _uniq.584 -> _uniq.310
+          • FVarAlias a: _uniq.588 -> _uniq.315
+          • FVarAlias α: _uniq.587 -> _uniq.313
           • ?m x α a : α @ ⟨9, 18⟩-⟨9, 19⟩ @ Lean.Elab.Term.elabHole
           • [.] Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
           • Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
@@ -71,8 +71,8 @@ a : α
           • Fam2.nat n : Fam2 Nat Nat @ ⟨10, 4⟩†-⟨10, 14⟩
             • n (isBinder := true) : Nat @ ⟨10, 13⟩-⟨10, 14⟩
           • a (isBinder := true) : Nat @ ⟨8, 2⟩†-⟨10, 19⟩†
-          • FVarAlias a: _uniq.616 -> _uniq.312
-          • FVarAlias n: _uniq.615 -> _uniq.310
+          • FVarAlias a: _uniq.619 -> _uniq.315
+          • FVarAlias n: _uniq.618 -> _uniq.313
           • n : Nat @ ⟨10, 18⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabIdent
             • [.] n : some Nat @ ⟨10, 18⟩-⟨10, 19⟩
             • n : Nat @ ⟨10, 18⟩-⟨10, 19⟩

diff --git a/tests/lean/run/ack.lean b/tests/lean/run/ack.lean
@@ -5,14 +5,16 @@ def ack : Nat → Nat → Nat
 termination_by a b => (a, b)
 
 /--
-info: [reduction] unfolded declarations (max: 1725, num: 4):
-  [reduction] Nat.rec ↦ 1725
-  [reduction] Eq.rec ↦ 1114
-  [reduction] Acc.rec ↦ 1050
-  [reduction] PSigma.rec ↦ 513[reduction] unfolded reducible declarations (max: 1577, num: 3):
-  [reduction] Nat.casesOn ↦ 1577
-  [reduction] Eq.ndrec ↦ 984
-  [reduction] PSigma.casesOn ↦ 513[kernel] unfolded declarations (max: 1193, num: 5):
+info: [reduction] unfolded declarations (max: 2567, num: 5):
+  [reduction] Nat.rec ↦ 2567
+  [reduction] Eq.rec ↦ 1517
+  [reduction] Acc.rec ↦ 1158
+  [reduction] Or.rec ↦ 770
+  [reduction] PSigma.rec ↦ 514[reduction] unfolded reducible declarations (max: 2337, num: 4):
+  [reduction] Nat.casesOn ↦ 2337
+  [reduction] Eq.ndrec ↦ 1307
+  [reduction] Or.casesOn ↦ 770
+  [reduction] PSigma.casesOn ↦ 514[kernel] unfolded declarations (max: 1193, num: 5):
   [kernel] Nat.casesOn ↦ 1193
   [kernel] Nat.rec ↦ 1065
   [kernel] Eq.ndrec ↦ 973

diff --git a/tests/lean/run/meta5.lean b/tests/lean/run/meta5.lean
@@ -28,11 +28,11 @@ info: [Meta.debug] ?_
 [Meta.debug] fun y =>
       let x := 0;
       x.add y
-[Meta.debug] ?_uniq.3019 : Nat →
+[Meta.debug] ?_uniq.3037 : Nat
+[Meta.debug] ?_uniq.3038 : Nat →
       Nat →
         let x := 0;
         Nat
-[Meta.debug] ?_uniq.3018 : Nat
 -/
 #guard_msgs in
 #eval tst1