fix tests

tests/lean/2505.lean.expected.out

@@ -1,3 +1,3 @@
+2505.lean:14:0-14:7: warning: declaration uses 'sorry'
 target : A (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))
 target' : A (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))
-2505.lean:14:0-14:7: warning: declaration uses 'sorry'

tests/lean/4089.lean.expected.out

@@ -8,6 +8,7 @@ def f (x_1 : obj) : obj :=
     let x_5 : obj := reset[2] x_1;
     let x_4 : obj := reuse x_5 in ctor_0[Prod.mk] x_3 x_2;
     ret x_4
+
 [reset_reuse]
 def Sigma.toProd._rarg (x_1 : obj) : obj :=
   case x_1 : obj of
@@ -20,6 +21,7 @@ def Sigma.toProd._rarg (x_1 : obj) : obj :=
 def Sigma.toProd (x_1 : ◾) (x_2 : ◾) : obj :=
   let x_3 : obj := pap Sigma.toProd._rarg;
   ret x_3
+
 [reset_reuse]
 def foo (x_1 : obj) : obj :=
   case x_1 : obj of
@@ -35,4 +37,4 @@ def foo (x_1 : obj) : obj :=
       let x_5 : obj := proj[0] x_3;
       let x_6 : obj := foo x_4;
       let x_7 : obj := reuse x_9 in ctor_1[List.cons] x_5 x_6;
-      ret x_7
+      ret x_7

tests/lean/4240.lean.expected.out

@@ -23,4 +23,4 @@ def isSomeWithInstanceNat._boxed (x_1 : obj) : obj :=
   let x_2 : u8 := isSomeWithInstanceNat x_1;
   dec x_1;
   let x_3 : obj := box x_2;
-  ret x_3
+  ret x_3

tests/lean/Process.lean.expected.out

@@ -1,6 +1,5 @@
-hi!
-<stdin>:1:0: warning: using 'exit' to interrupt Lean
 1
+hi!
 0
 "ho!\n"
 "hu!\n"
@@ -9,6 +8,7 @@ flush of broken pipe failed
 100000
 0
 0
+<stdin>:1:0: warning: using 'exit' to interrupt Lean
 0
 0
 none

tests/lean/computedFieldsCode.lean.expected.out

@@ -106,6 +106,7 @@ def Exp.hash._override._boxed (x_1 : obj) : obj :=
   dec x_1;
   let x_3 : obj := box x_2;
   ret x_3
+
 [result]
 def f._closed_1 : obj :=
   let x_1 : u32 := 10;
@@ -124,6 +125,7 @@ def f._closed_3 : u64 :=
 def f : u64 :=
   let x_1 : u64 := f._closed_3;
   ret x_1
+
 [result]
 def g (x_1 : @& obj) : u8 :=
   case x_1 : obj of
@@ -138,6 +140,7 @@ def g._boxed (x_1 : obj) : obj :=
   dec x_1;
   let x_3 : obj := box x_2;
   ret x_3
+
 [result]
 def hash' (x_1 : @& obj) : obj :=
   case x_1 : obj of
@@ -161,6 +164,7 @@ def hash'._boxed (x_1 : obj) : obj :=
   let x_2 : obj := hash' x_1;
   dec x_1;
   ret x_2
+
 [result]
 def getAppFn (x_1 : @& obj) : obj :=
   case x_1 : obj of
@@ -175,11 +179,12 @@ def getAppFn._boxed (x_1 : obj) : obj :=
   let x_2 : obj := getAppFn x_1;
   dec x_1;
   ret x_2
+
 [result]
 def Exp.f (x_1 : @& obj) : obj :=
   let x_2 : obj := getAppFn x_1;
   ret x_2
 def Exp.f._boxed (x_1 : obj) : obj :=
   let x_2 : obj := Exp.f x_1;
   dec x_1;
-  ret x_2
+  ret x_2

tests/lean/csimpAttr.lean.expected.out

@@ -1,6 +1,7 @@
+csimpAttr.lean:7:2-7:7: error: invalid 'csimp' theorem, only constant replacement theorems (e.g., `@f = @g`) are currently supported.
 
 [init]
 def f (x_1 : obj) : obj :=
   let x_2 : obj := Nat.add x_1 x_1;
   let x_3 : obj := Nat.add x_2 x_2;
-  ret x_3csimpAttr.lean:7:2-7:7: error: invalid 'csimp' theorem, only constant replacement theorems (e.g., `@f = @g`) are currently supported.
+  ret x_3

tests/lean/csimpAttrAppend.lean.expected.out

@@ -3,4 +3,4 @@
 def f (x_1 : obj) (x_2 : obj) (x_3 : obj) : obj :=
   let x_4 : obj := List.appendTR._rarg x_1 x_2;
   let x_5 : obj := List.appendTR._rarg x_4 x_3;
-  ret x_5
+  ret x_5

tests/lean/dbgMacros.lean.expected.out

@@ -1,10 +1,10 @@
 PANIC at f dbgMacros:2:14: unexpected zero
-PANIC at g dbgMacros:10:14: unreachable code has been reached
-PANIC at h dbgMacros:16:0: assertion violation: x != 0
 0
 9
+PANIC at g dbgMacros:10:14: unreachable code has been reached
 0
 0
+PANIC at h dbgMacros:16:0: assertion violation: x != 0
 0
 f2, x: 10
 11

tests/lean/doubleReset.lean.expected.out

@@ -34,4 +34,4 @@ def applyProjectionRules._rarg (x_1 : obj) (x_2 : obj) : obj :=
   ret x_5
 def applyProjectionRules (x_1 : ◾) (x_2 : ◾) (x_3 : ◾) : obj :=
   let x_4 : obj := pap applyProjectionRules._rarg;
-  ret x_4
+  ret x_4

tests/lean/etaReducedMvarAssignments.lean.expected.out

@@ -1,4 +1,4 @@
-Pi.hasLe : LE ((i : ι) → α i)
-[Meta.isDefEq.assign] ✅ ?m i := α i
-  [Meta.isDefEq.assign.beforeMkLambda] ?m [i] := α i
-  [Meta.isDefEq.assign.checkTypes] ✅ (?m : ι → Type ?u) := (α : ι → Type v)
+Pi.hasLe : LE ((i : ι) → α i)
+[Meta.isDefEq.assign] ✅ ?m i := α i
+  [Meta.isDefEq.assign.beforeMkLambda] ?m [i] := α i
+  [Meta.isDefEq.assign.checkTypes] ✅ (?m : ι → Type ?u) := (α : ι → Type v)

tests/lean/listLength.lean.expected.out

@@ -5,4 +5,4 @@ def f (x_1 : obj) : obj :=
   let x_3 : obj := List.lengthTRAux._rarg x_1 x_2;
   let x_4 : obj := 2;
   let x_5 : obj := Nat.mul x_4 x_3;
-  ret x_5
+  ret x_5

tests/lean/lit_values.lean.expected.out

@@ -3,10 +3,10 @@
 (some 2)
 (some -2)
 (some a)
+some "hello"
 (some (⟨5, 3⟩))
 (some (⟨12, 0x003#12⟩))
 (some 2)
 (some 2)
 (some 2)
 (some 2)
-some "hello"

tests/lean/unboxStruct.lean.expected.out

@@ -7,4 +7,4 @@ def test2._boxed (x_1 : obj) (x_2 : obj) : obj :=
   let x_3 : u32 := unbox x_1;
   dec x_1;
   let x_4 : obj := test2 x_3 x_2;
-  ret x_4
+  ret x_4

tests/lean/updateExprIssue.lean.expected.out

@@ -1,4 +1,5 @@
 
+
 [init]
 def sefFn (x_1 : obj) (x_2 : obj) : obj :=
   case x_1 : obj of