Update a few tests

Author: nomeata

tests/lean/run/issue2171.lean

@@ -3,7 +3,7 @@ def g (n : Nat) : Nat :=
     1
   else
     4 + g (n - 1)
-  termination_by n
+  termination_by (n,0)
   decreasing_by simp_wf; omega
 
 example : g 10000 = id g (id 10000) := rfl

tests/lean/run/letToHaveCleanup.lean

@@ -168,7 +168,7 @@ def fnWFRec (n : Nat) : let α := Nat; α :=
   | 0 => 0
   | n + 1 => id (let m := n + 1; m * fnWFRec (n / 2))
 /--
-info: @[irreducible] def fnWFRec : Nat →
+info: def fnWFRec : Nat →
   have α : Type := Nat;
   α :=
 WellFounded.Nat.fix (fun x => x) fun n a =>

tests/lean/run/mutwf2.lean

@@ -11,14 +11,14 @@ mutual
 end
 
 /--
-info: @[irreducible] def Ex1.isEven : Nat → Bool :=
+info: def Ex1.isEven : Nat → Bool :=
 fun a => isEven._mutual (PSum.inl a)
 -/
 #guard_msgs in
 #print isEven
 
 /--
-info: @[irreducible] def Ex1.isOdd : Nat → Bool :=
+info: def Ex1.isOdd : Nat → Bool :=
 fun a => isEven._mutual (PSum.inr a)
 -/
 #guard_msgs in

tests/lean/run/structuralEqn6.lean

@@ -34,7 +34,7 @@ where
 
 /--
 info: equations:
-@[defeq] theorem trailingZeros'.aux.eq_1 : ∀ (i : Int) (hi : i ≠ 0) (acc k_2 : Nat) (x_1 : k_2 + 1 ≠ 0)
+theorem trailingZeros'.aux.eq_1 : ∀ (i : Int) (hi : i ≠ 0) (acc k_2 : Nat) (x_1 : k_2 + 1 ≠ 0)
   (hk_2 : i.natAbs ≤ k_2 + 1),
   trailingZeros'.aux k_2.succ i hi hk_2 acc =
     if h : i % 2 = 0 then trailingZeros'.aux k_2 (i / 2) ⋯ ⋯ (acc + 1) else acc
@@ -77,7 +77,7 @@ where
 
 /--
 info: equations:
-@[defeq] theorem trailingZeros2'.aux.eq_1 : ∀ (i : Int) (hi : i ≠ 0) (acc k_2 : Nat) (hk_2 : i.natAbs ≤ k_2 + 1),
+theorem trailingZeros2'.aux.eq_1 : ∀ (i : Int) (hi : i ≠ 0) (acc k_2 : Nat) (hk_2 : i.natAbs ≤ k_2 + 1),
   trailingZeros2'.aux k_2.succ i hi hk_2 acc =
     if h : i % 2 = 0 then trailingZeros2'.aux k_2 (i / 2) ⋯ ⋯ (acc + 1) else acc
 @[defeq] theorem trailingZeros2'.aux.eq_2 : ∀ (i : Int) (hi : i ≠ 0) (acc : Nat) (hk_2 : i.natAbs ≤ 0),

tests/lean/run/wfEqns5.lean

@@ -8,7 +8,7 @@ termination_by n => n
 info: equations:
 @[defeq] theorem foo.eq_1 : foo 0 0 = 0
 theorem foo.eq_2 : ∀ (x : Nat), (x = 0 → False) → foo 0 x = x
-@[defeq] theorem foo.eq_3 : ∀ (x n : Nat), foo n.succ x = foo n x
+theorem foo.eq_3 : ∀ (x n : Nat), foo n.succ x = foo n x
 -/
 #guard_msgs in
 #print equations foo
@@ -58,7 +58,7 @@ info: equations:
     match x with
     | 0 => 0
     | m => m
-@[defeq] theorem bar.eq_2 : ∀ (x n : Nat), bar n.succ x = bar n x
+theorem bar.eq_2 : ∀ (x n : Nat), bar n.succ x = bar n x
 -/
 #guard_msgs in
 #print equations bar
@@ -125,7 +125,7 @@ info: equations:
     match x with
     | 0 => 0
     | m => m
-@[defeq] theorem Structural.bar.eq_2 : ∀ (x n : Nat), bar n.succ x = bar n x
+theorem Structural.bar.eq_2 : ∀ (x n : Nat), bar n.succ x = bar n x
 -/
 #guard_msgs in
 #print equations bar

tests/lean/wfrecUnusedLet.lean.expected.out

@@ -1,4 +1,4 @@
-@[irreducible] def f : Nat → Nat :=
+def f : Nat → Nat :=
 WellFounded.Nat.fix (fun x => x) fun n a =>
   if h : n = 0 then 1
   else

tests/pkg/module/Module/ImportedAll.lean

@@ -77,7 +77,7 @@ info: private theorem f_struct.eq_unfold : f_struct = fun x =>
 -/
 #guard_msgs in #print sig f_struct.eq_unfold
 
-/-- info: private theorem f_wfrec.eq_1 : ∀ (x : Nat), f_wfrec 0 x = x -/
+/-- info: @[defeq] private theorem f_wfrec.eq_1 : ∀ (x : Nat), f_wfrec 0 x = x -/
 #guard_msgs(pass trace, all) in #print sig f_wfrec.eq_1
 
 /--

tests/pkg/module/Module/NonModule.lean

@@ -26,7 +26,7 @@ info: theorem f_struct.eq_unfold : f_struct = fun x =>
 -/
 #guard_msgs in #print sig f_struct.eq_unfold
 
-/-- info: theorem f_wfrec.eq_1 : ∀ (x : Nat), f_wfrec 0 x = x -/
+/-- info: @[defeq] theorem f_wfrec.eq_1 : ∀ (x : Nat), f_wfrec 0 x = x -/
 #guard_msgs(pass trace, all) in #print sig f_wfrec.eq_1
 
 /--