From 47c09ac36cc420878220d196d2191e1e8547faf4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 30 Oct 2023 15:35:49 -0700 Subject: [PATCH] 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 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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