commit: ad593b36d9eeac954a6b1810385d3707bada87a7

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

Sat Jan 04 03:18:43 2025 +0100
committer: GitHub <noreply@github.com>

Sat Jan 04 02:18:43 2025 +0000
tree: 4a60e59dd938844e7ea85e6ce096fee3e4dc8c09
parent: 28a70987284f403fd2d17812d39ee3fbecaa5418 [diff]

feat: add support for `match`-expressions to `grind` (#6521)

This PR adds support for activating relevant `match`-equations as
E-matching theorems. It uses the `match`-equation lhs as the pattern.

11 files changed

tree: 4a60e59dd938844e7ea85e6ce096fee3e4dc8c09

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