commit: 2c13d145dc05899f8ac5928253787d8a495f6c2b

[log]
author: Parth Shastri <31370288+cppio@users.noreply.github.com>

Tue Jul 01 09:30:31 2025 -0400
committer: GitHub <noreply@github.com>

Tue Jul 01 13:30:31 2025 +0000
tree: 30e6e6f59c1c956265aff22c9403d44b69b943c5
parent: 232443371bd7f4c1cef5c64aff6cbdd945afeef5 [diff]

fix: match against app fn for reducing recursor in `whnfCore` (#9090)

This PR fixes a bug in `whnfCore` where it would fail to reduce
applications of recursors/auxiliary defs.

Closes #9089

src/Lean/Meta/WHNF.lean[diff]
tests/lean/run/9089.lean[Added - diff]

2 files changed

tree: 30e6e6f59c1c956265aff22c9403d44b69b943c5

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.