commit: 2d1a86edf52d96e1d02ffeec475addeb58ec3ce5

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

Fri Sep 05 09:01:19 2025 -0700
committer: Leonardo de Moura <leomoura@amazon.com>

Fri Sep 05 09:09:43 2025 -0700
tree: dece7271e8877a9800e9c751493f5c833c721999
parent: 974c649e2eca4d63e8d1a9606322175220b91702 [diff]

fix: panic in `grind ring`

This PR fixes a panic in `grind ring` exposed by #10242. `grind ring`
should not assume that all normalizations have been applied, because
some subterms cannot be rewritten by `simp` due to typing constraints.
Moreover, `grind` uses `preprocessLight` in a few places, and it skips
the simplifier/normalizer.

Closes #10242

2 files changed

tree: dece7271e8877a9800e9c751493f5c833c721999

README.md

This is the repository for Lean 4.

About

Installation

See Setting Up Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.