commit: 28d96f03966638241f390d930ffaed64c0585e25

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

Sat Sep 20 07:38:26 2025 -0700
committer: Leonardo de Moura <leomoura@amazon.com>

Sat Sep 20 07:41:21 2025 -0700
tree: 88d0360fa7e02969a601c39dd4e9ded0fba4568e
parent: 4379002d0582ae96d7fc6ccf5921ff4e9aa7239e [diff]

fix: `infer_let` in the kernel

This PR fixes the dead `let` elimination code in the kernel's
`infer_let` function.

Closes #10475

src/kernel/type_checker.cpp[diff]
tests/lean/run/10475.lean[Added - diff]

2 files changed

tree: 88d0360fa7e02969a601c39dd4e9ded0fba4568e

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.