commit: b7cd87e624198f677502919b5164a1ce01fa8d41

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

Sun Oct 25 02:41:30 2026 +0000
committer: Leonardo de Moura <leomoura@amazon.com>

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

perf: implement `Expr.instantiateLevelParams` natively

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`.

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.