commit: 9057b916edf12e9db232a8ce98250a893d03d941

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

Tue Oct 27 00:22:36 2026 +0000
committer: Leonardo de Moura <leomoura@amazon.com>

Tue Oct 27 00:22:36 2026 +0000
tree: aff22c68a2ab5b4f44d3e6f76ce05053dd49edca
parent: 7813005650fd2a6601613488fe5486bb30b9c4f6 [diff]

perf: skip the imported map again for local constants in `Environment.hasUnsafe`

This PR makes `Environment.hasUnsafe` look up constants that are not imported with `findAsyncCore?`, as `findAsync?` would search the imported map again, and documents why imported constants are looked up directly.

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

src/Lean/Environment.lean[diff]

1 file changed

tree: aff22c68a2ab5b4f44d3e6f76ce05053dd49edca

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.