commit: f7bc692dbb1e5f1220d537d35ccb9889c7504fb1

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

Wed Jan 15 08:22:44 2025 -0800
committer: Leonardo de Moura <leomoura@amazon.com>

Wed Jan 15 08:22:44 2025 -0800
tree: 04deebfc701b362a8cba4a645b4cf2e1d2ec7b2b
parent: 6665837232cc8464eb2d41534ce7e50db6fda674 [diff]

fix: improve E-matching pattern selection heuristics

This PR improves the E-matching pattern selection heuristics in the
`grind` tactic. They now take into account type predicates and transformers.

2 files changed

tree: 04deebfc701b362a8cba4a645b4cf2e1d2ec7b2b

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