commit: 1a573bda1b68f9eb5ef63e588c405ad6a5301823

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

Sat Oct 24 16:59:27 2026 +0000
committer: Leonardo de Moura <leomoura@amazon.com>

Sat Oct 24 17:04:12 2026 +0000
tree: a4d8ee5f0278532803faf56263670d1fd1ea87ae
parent: d0129c22d718501aa68d2a029c791ae405931260 [diff]

perf: speed up `Expr.cleanupAnnotations`

This PR speeds up `Expr.cleanupAnnotations`, which `match_expr` and `let_expr` call on the discriminant and after every argument they peel.

It now inspects the root of the expression once, instead of applying `consumeMData` and `consumeTypeAnnotations` and comparing the result with `Expr.eqv` to detect a fixpoint. The PR also fixes the docstring examples of `cleanupAnnotations` and `consumeTypeAnnotations`.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

src/Lean/Expr.lean[diff]
tests/elab/cleanupAnnotations.lean[Added - diff]

2 files changed

tree: a4d8ee5f0278532803faf56263670d1fd1ea87ae

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.