commit: b37262150a22e1b5a741fd38192f2ca7b8974a67

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

Wed Jun 19 14:46:51 2024 -0700
committer: Leonardo de Moura <leomoura@amazon.com>

Wed Jun 19 14:46:51 2024 -0700
tree: c1c7a55a72baa927a5ea83269128d52fe93a398c
parent: bc047b8530f76f75c4456192b3ca24ad28c85420 [diff]

feat: `open _root_.<namespace>`

closes #3045

src/Lean/ResolveName.lean[diff]
tests/lean/run/3045.lean[Added - diff]

2 files changed

tree: c1c7a55a72baa927a5ea83269128d52fe93a398c

README.md

This is the repository for Lean 4.

About

Installation

See Setting Up Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean (documentation source: doc/make/index.md).