commit: 5a4ca257eee2ca4d228e837648542b2cf438d671

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

Thu Jan 08 21:43:47 2026 -0800
committer: Leonardo de Moura <leomoura@amazon.com>

Thu Jan 08 22:07:19 2026 -0800
tree: 84608b1a71a4bcef829e3a3729bcf47b6472e6e1
parent: 7d5a96941e5b92d2f5956f7adf078dfc253bf4ba [diff]

feat: `simpForall` and `simpArrow` for `Sym.simp`

This PR implements `simpForall` and `simpArrow` for `Sym.simp`.

src/Init/SimpLemmas.lean[diff]
src/Lean/Meta/Sym/Simp/Funext.lean[diff]
src/Lean/Meta/Sym/Simp/Main.lean[diff]
tests/bench/sym/meta_simp_4.lean[Added - diff]
tests/bench/sym/simp_4.lean[Added - diff]

5 files changed

tree: 84608b1a71a4bcef829e3a3729bcf47b6472e6e1

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.