perf: inline `EnvExtension.getStateImpl` `getStateImpl` needs an `Inhabited` instance only to panic on an invalid extension index, but as an out-of-line call it made its callers build the instance first. `PersistentEnvExtension.getModuleEntries`, used by every lookup in an imported module's entries, thus allocated and freed an `Inhabited (PersistentEnvExtensionState α σ)` on each call. Inlined, the instance is only built on the panic path. No public IR signature changes. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This is the repository for Lean 4.
See Install Lean.
Please read our Contribution Guidelines first.
See Building Lean.