commit: 461ea67cb7fe71ab7463ecb54436936e2c48c04a

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

Thu Dec 12 16:06:39 2024 -0800
committer: Leonardo de Moura <leomoura@amazon.com>

Thu Dec 12 16:08:01 2024 -0800
tree: b525cc0c802623254a73292bb598b98f64edb977
parent: 48be424eaa2ae06972e9cfec4d355906b532204d [diff]

fix: unused `let_fun` elimination in `simp`

This PR fixes a bug in the simplifier. It was producing terms with
loose bound variables when eliminating unused `let_fun` expressions.

This issue was affecting the example at #6374. The example is now
timing out.

2 files changed

tree: b525cc0c802623254a73292bb598b98f64edb977

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 (documentation source: doc/make/index.md).