commit: 6b2fc8de7b94bab3d8bffe008f4a4cb8f307e00f

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

Fri Feb 06 16:11:59 2026 -0800
committer: Leonardo de Moura <leomoura@amazon.com>

Fri Feb 06 16:11:59 2026 -0800
tree: 235a5352b62aeb3ae7b9abd20237937ce9dd5e0c
parent: 9f2f33bd659770a25df18a988e3df29f70fc7845 [diff]

fix: simp `have` in `Sym`

This PR fixes a proof construction bug in `Sym.simp`.

Closes #12336

src/Lean/Meta/Sym/Simp/Have.lean[diff]
tests/lean/run/sym_cbv_12336.lean[Added - diff]

2 files changed

tree: 235a5352b62aeb3ae7b9abd20237937ce9dd5e0c

README.md

This is the repository for Lean 4.

About

Installation

See Install Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.