commit: 270423a41427cef1782bdc104218972898743562

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

Mon Jul 13 18:03:47 2026 +0000
committer: Leonardo de Moura <leomoura@amazon.com>

Mon Jul 13 18:03:47 2026 +0000
tree: 885512534917f10617c4f205370be288ae23bcda
parent: 373c37ead3c0dd57f3a7ab0329157088e0907adb [diff]

fix: boostrapping issue in `grind`

This PR fixes a bootstrapping issue in the `grind` normalizer.
The `BitVec.ofNatLT` normalization theorem must be added to the `grind` normalization set **before** we process `Init/Data/BitVec/Lemmas.lean`.
Otherwise, patterns are not properly normalized.

7 files changed

tree: 885512534917f10617c4f205370be288ae23bcda

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.