New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

`#where` doesn't print `open scoped` #12606

Closed

fpvandoorn opened this issue May 2, 2024 · 1 comment

Member

fpvandoorn commented May 2, 2024 •

edited

Loading

import Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
open scoped Topology
#where -- In root namespace with initial scope

fpvandoorn mentioned this issue

#where doesn't print open scoped leanprover-community/batteries#778

Open

Contributor

kim-em commented May 13, 2024

Closed in favour of leanprover-community/batteries#778

kim-em closed this as completed

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment