commit: 5788d2245ec069ea9a60880153f04cc22b3a4bc8

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

Mon Jan 13 17:38:35 2025 -0800
committer: Leonardo de Moura <leomoura@amazon.com>

Mon Jan 13 17:52:51 2025 -0800
tree: ba50f0dfe11194f049105bf1aa761b7f1fe848fa
parent: f57745e9d47144505544fcaeb12c72cb7881ea47 [diff]

chore: display E-matching theorems in `goalToMessageData`

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