commit: d6f0c324c31d81191e91ef4294f55fbd66190b85

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

Mon Jan 13 18:25:30 2025 -0800
committer: GitHub <noreply@github.com>

Tue Jan 14 02:25:30 2025 +0000
tree: ba50f0dfe11194f049105bf1aa761b7f1fe848fa
parent: f57745e9d47144505544fcaeb12c72cb7881ea47 [diff]

chore: display E-matching theorems in `goalToMessageData` (#6635)

This PR includes the activated E-matching theorems and their patterns in
`goalToMessageData`

src/Lean/Meta/Tactic/Grind/PP.lean[diff]

1 file changed

tree: ba50f0dfe11194f049105bf1aa761b7f1fe848fa

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