commit: 468096912bad91968577453b7f75c20a0b5a3025

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

Fri Jul 10 14:02:11 2026 +0000
committer: Leonardo de Moura <leomoura@amazon.com>

Fri Jul 10 07:14:54 2026 -0700
tree: 394648d7aa0528038ec2673e52e032fc73eddf68
parent: da19ea085d7cdba0131ec59b4f678b0910304878 [diff]

perf: avoid unnecessary `modifyEnv`

This PR implements a minor optimization at `withExporting/withoutExporting`.
When they call `modifyEnv` to toggle `Environment.isExporting`, and
`MonadEnv` `MetaM`'s `modifyEnv` wipes all `Core` and `Meta` caches.

chore: use `old`

src/Lean/Environment.lean[diff]

1 file changed

tree: 394648d7aa0528038ec2673e52e032fc73eddf68

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.