commit: 72705d854052ef0ae0347df65e0ba680720cc9bf

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

Mon Aug 11 11:04:40 2025 -0700
committer: Leonardo de Moura <leomoura@amazon.com>

Mon Aug 11 11:08:21 2025 -0700
tree: 331bed9f8b65e842ae04b5492f612cf8075341d6
parent: b8531665758f4a7e31d283d8adc6c377ecd83573 [diff]

fix: remove `inShareCommon` filter used in `grind`

This PR removes the `inShareCommon` quick filter used in `grind` preprocessing steps. `shareCommon` is no longer used only for fully preprocessed terms.

closes #9830

4 files changed

tree: 331bed9f8b65e842ae04b5492f612cf8075341d6

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.