commit: c811617e71a1fa980830af00dfc92e49b53f5dc8

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

Mon Dec 30 07:56:17 2024 -0800
committer: Leonardo de Moura <leomoura@amazon.com>

Mon Dec 30 07:58:21 2024 -0800
tree: 03ef05da8ed5c050519359041dfebb7530c93518
parent: 9b28c5879a77f9f0212a7f39ea83f56c71abda42 [diff]

fix: internalize nested ground patterns when activating ematch theorems

This PR internalize nested ground patterns when activating ematch
theorems in the (WIP) `grind` tactic.

4 files changed

tree: 03ef05da8ed5c050519359041dfebb7530c93518

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