chore: the previous commit exposed an issue with simp

`simp` was previously swallowing runtime exceptions and masking an
issue with this example.

`runT` is defined by well-founded recursion, but reducing the ground
term `runT x` takes a long time when `decide := true`.

Remark PR #2722 changes the `decide` default value to `false`.

When `decide := true`, we should probably have better diagnostics /
error messages for this kind of situation.

tests/lean/run/lazyUnfoldingPerfIssue.lean

@@ -18,7 +18,7 @@ theorem equivalent: Run.run x = Run.run x := by
   apply Eq.refl (runT x)
 
 example : Run.run x = Run.run x := by
-  simp [Run.run]
+  simp (config := { decide := false }) [Run.run]
 
 end Ex1