commit: 0e0236dddfd83cc83000944f05ff5fe27aed0bfc

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

Sat Oct 24 00:36:31 2026 +0000
committer: Leonardo de Moura <leomoura@amazon.com>

Sat Oct 24 02:28:02 2026 +0000
tree: bf4e92f028d1352033ed03eea3ec7012fc504ca5
parent: 44c734afcacf13b8322154f59fdb3c5955b2ee3b [diff]

perf: skip the `simp` preprocessor for `lia` div/mod facts

This PR makes `lia` add the linear facts it derives for `a / k` and `a % k` without running them through the `simp`-based preprocessor. These facts are linear combinations that `lia` normalizes itself.

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

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean[diff]

1 file changed

tree: bf4e92f028d1352033ed03eea3ec7012fc504ca5

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.