leanprover-community/batteries

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

fpvandoorn opened this issue · 0 comments

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.