diff --git a/tests/lean/run/lazyUnfoldingPerfIssue.lean b/tests/lean/run/lazyUnfoldingPerfIssue.lean index af4ecfe10a..64b773cf69 100644 --- a/tests/lean/run/lazyUnfoldingPerfIssue.lean +++ b/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