commit: 00ef231a6e03398c2ad3b577ab036f901ec88543

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

Tue Jan 07 19:10:11 2025 -0800
committer: GitHub <noreply@github.com>

Wed Jan 08 03:10:11 2025 +0000
tree: 240ceb692ab466b53707f2d0ae58c9be6cc19dda
parent: 9040108e2f069dcba488246424812649f37d9fca [diff]

feat: split on `match`-expressions in the `grind` tactic (#6569)

This PR adds support for case splitting on `match`-expressions in
`grind`.
We still need to add support for resolving the antecedents of
`match`-conditional equations.

9 files changed

tree: 240ceb692ab466b53707f2d0ae58c9be6cc19dda

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).