commit: 19e1fe55f33a8aadc4243da32828b70a4b4677cc

[log]
author: Joachim Breitner <mail@joachim-breitner.de>

Wed Dec 10 00:36:46 2025 +0100
committer: GitHub <noreply@github.com>

Tue Dec 09 23:36:46 2025 +0000
tree: 88764427f2b8a13df60bd220b1df2a66967c6ab8
parent: 5bf5c73f740e16148c105c1d52381e01bdfa6418 [diff]

perf: do not consult isNoConfusion in whnf (#11571)

This PR lets `whnf` not consult `isNoConfusion`, to speed up this hot
path a bit.

src/Lean/AuxRecursor.lean[diff]
src/Lean/Meta/WHNF.lean[diff]
src/library/CMakeLists.txt[diff]
src/library/aux_recursors.cpp[Deleted - diff]
src/library/aux_recursors.h[Deleted - diff]
src/library/constructions/cases_on.cpp[diff]

6 files changed

tree: 88764427f2b8a13df60bd220b1df2a66967c6ab8

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.