commit: 0b2e02c33fc4ca805900cff9858d202fa748cb2c

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

Sun Jan 05 08:03:15 2025 -0800
committer: Leonardo de Moura <leomoura@amazon.com>

Sun Jan 05 08:03:15 2025 -0800
tree: d00d1f76acd8e10ebfbbb0df8970bceef407d7f9
parent: dc5c8097b5ca053dd49b5de246add54c3e999734 [diff]

fix: allow projections in E-matching patterns

This PR ensures that users can utilize projections in E-matching
patterns within the `grind` tactic.

2 files changed

tree: d00d1f76acd8e10ebfbbb0df8970bceef407d7f9

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