commit: c5d8a378ba77d655e25c55f1fcf8d1dfe9ee12e1

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

Tue Dec 31 09:26:33 2024 -0800
committer: Leonardo de Moura <leomoura@amazon.com>

Tue Dec 31 09:26:33 2024 -0800
tree: 376b7ae8d588ac22a55ec1851abdf41e6b46b841
parent: 2c87905d77b707c3283c1de759fd63269ac386a1 [diff]

feat: instantiate ematch theorems using assignment

This PR implements `Grind.EMatch.instantiateTheorem` in the (WIP)
`grind` tactic.

4 files changed

tree: 376b7ae8d588ac22a55ec1851abdf41e6b46b841

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