max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: the previous commit exposed an issue with simp

Browse source 
`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.
This commit is contained in:
Leonardo de Moura 2023-10-30 15:35:49 -07:00 • committed by Leonardo de Moura
parent 4afcdeb771
commit 47c09ac36c
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/lean/run/lazyUnfoldingPerfIssue.lean
View file

@ -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