commit: 2b68e5ce1befb06f08a8003e8ab74453a786fe34

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

Sat Oct 24 22:28:26 2026 +0000
committer: Leonardo de Moura <leomoura@amazon.com>

Sat Oct 24 22:28:26 2026 +0000
tree: ac9fb8694bf0918c6c0cb6cb60bf4cd74656908a
parent: fe18ef334591af752d201958c501a50eef057c8a [diff]

fix: give the `/` and `%` facts of cutsat the generation of `a`

`pushDivModFact` added the facts about `a / k` and `a % k` with generation 0, so their terms got generation 0 even when `a` came from E-matching.

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

2 files changed

tree: ac9fb8694bf0918c6c0cb6cb60bf4cd74656908a

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.