commit: fe5bd839fd64401a94a53d7958af9caab440ee87

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

Sun Oct 25 02:50:17 2026 +0000
committer: GitHub <noreply@github.com>

Sun Oct 25 02:50:17 2026 +0000
tree: fdfb50bfb3c0a51657c8292faab541181424110f
parent: 6cffe2f4cc08a629039443cafb6afb42da78811d [diff]

perf: implement `Expr.instantiateLevelParams` natively (#15928)

This PR implements `Expr.instantiateLevelParams` in C++. It previously
ran `Expr.replace` with a Lean closure called at every visited node.
Levels containing `max`/`imax`/`succ` over parameters are still
instantiated by `Level.instantiateParams`.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>

3 files changed

tree: fdfb50bfb3c0a51657c8292faab541181424110f

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.