`#where` doesn't print `open scoped`
fpvandoorn opened this issue · 0 comments
fpvandoorn commented
import Std.Tactic.Where
open scoped Nat
#where -- In root namespace with initial scope
Duplicate of leanprover-community/mathlib4#12606 because I didn't realize #where
is defined here.