lean4-htt/tests/bench/sym
Leonardo de Moura 78c9a01bb2
feat: check Sym.simp thresholds (#11890)
This PR ensures that `Sym.simp` checks thresholds for maximum recursion
depth and maximum number of steps. It also invokes `checkSystem`.
Additionally, this PR simplifies the main loop. Assigned metavariables
and `zetaDelta` reduction are now handled by installing `pre`/`post`
methods.
2026-01-04 04:27:46 +00:00
..
meta_simp_1.lean
simp_1.lean feat: check Sym.simp thresholds (#11890) 2026-01-04 04:27:46 +00:00