commit: 59bf20f4be9c45841c62e7acca79c1557c18394c

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

Fri May 24 18:00:13 2024 -0700
committer: Leonardo de Moura <leomoura@amazon.com>

Fri May 24 18:00:13 2024 -0700
tree: 1e3a42dd7a20be57a6b6341ee633ca29540b8082
parent: b0c1112471a3f38859d9738184d21132b7d9cd0c [diff]

fix: do not include internal `match` equational theorems at simp trace

closes #4251

src/Lean/Elab/Tactic/Simp.lean[diff]
src/Lean/Meta/Match/MatchEqsExt.lean[diff]
tests/lean/run/4251.lean[Added - diff]

3 files changed

tree: 1e3a42dd7a20be57a6b6341ee633ca29540b8082

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