commit: 108bf119048d4159a9561b469d660c5d7dc64c40

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

Thu Jan 02 07:42:22 2025 -0800
committer: Leonardo de Moura <leomoura@amazon.com>

Thu Jan 02 07:42:43 2025 -0800
tree: 3fe7ce47656decf55f95b80e31068049ba3ffe05
parent: 092449adb8488a8fcbbebf9fdfcec38deef1eb81 [diff]

fix: missing case in `checkParents`

This PR fixes a bug in the sanity checkers for the `grind` tactic.

src/Lean/Meta/Tactic/Grind/Inv.lean[diff]
tests/lean/run/grind_ematch2.lean[Added - diff]

2 files changed

tree: 3fe7ce47656decf55f95b80e31068049ba3ffe05

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 (documentation source: doc/make/index.md).