commit: 59dd9c829cd42ff28f8686a6911527920f1b562e

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

Thu Oct 23 16:55:14 2025 -0700
committer: Leonardo de Moura <leomoura@amazon.com>

Thu Oct 23 17:00:20 2025 -0700
tree: f385a5b59aac3783fdc9337c87c77730a50818d0
parent: 6d665f3e914dee21b4544ff8a380148300d08799 [diff]

fix: missing `processNewFacts` at solver tactics

This PR ensures solver `grind` tactics (e.g., `ac`, `ring`, `lia`,
etc) process pending facts after making progress.

src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean[diff]

1 file changed

tree: f385a5b59aac3783fdc9337c87c77730a50818d0

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.