mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
2f3d0ee6ad
This PR adds a `set_option cbv.maxSteps N` option that controls the maximum number of simplification steps the `cbv` tactic performs. Previously the limit was hardcoded to the `Sym.Simp.Config` default of 100,000 with no way for users to override it. The option is threaded through `cbvCore`, `cbvEntry`, `cbvGoal`, and `cbvDecideGoal`. 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
13 lines
358 B
Lean4
13 lines
358 B
Lean4
set_option cbv.warning false
|
|
|
|
-- Default limit works on a normal computation
|
|
example : (List.replicate 10 1).length = 10 := by cbv
|
|
|
|
-- Low limit triggers "maximum number of steps exceeded"
|
|
set_option cbv.maxSteps 10 in
|
|
/--
|
|
error: `simp` failed: maximum number of steps exceeded
|
|
-/
|
|
#guard_msgs (error) in
|
|
example : (List.replicate 10 1).length = 10 := by cbv
|