commit: eb649d890f84429f45c0d281c9d2707ca7c95617

[log]
author: Leonardo de Moura <leomoura@amazon.com>

Mon Nov 02 02:43:09 2026 +0000
committer: Leonardo de Moura <leomoura@amazon.com>

Mon Nov 02 02:43:09 2026 +0000
tree: 3b4cb809e1f06140787af5c5fb32e62e4c95dd90
parent: bbf92e1a55fd46bb109063ed40abea4bdf631ffd [diff]

perf: skip `acLt` for non-permutation theorems in `Sym.dsimp`

This PR fixes `sym => dsimp` timing out on large, deeply nested terms that `sym => simp` handles quickly.

Closes #15938

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

src/Lean/Meta/Sym/DSimp/Rewrite.lean[diff]
tests/elab/sym_dsimp_15938.lean[Added - diff]

2 files changed

tree: 3b4cb809e1f06140787af5c5fb32e62e4c95dd90

README.md

This is the repository for Lean 4.

About

Installation

See Install Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.