commit: a8d2234799becf5a315422a56c880316864ddbd9

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

Thu Jul 16 02:26:37 2026 +0000
committer: Leonardo de Moura <leomoura@amazon.com>

Thu Jul 16 02:26:37 2026 +0000
tree: 3645a81392e29dab681371b8c07144ee4b71bc97
parent: ee0963c2bd280dd6ccdca1f6cd544cb627678a48 [diff]

test: add regression test for `grind?` dropping `cases` params

This PR adds a regression test for #13828: `grind?` suggestions used to omit `cases` parameters (e.g., `cases Bool`), producing suggestions that failed during replay. The issue was fixed by #14022.

Closes #13828

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

tests/elab/grind_13828.lean[Added - diff]

1 file changed

tree: 3645a81392e29dab681371b8c07144ee4b71bc97

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.