batteries
batteries copied to clipboard
`#where` doesn't print `open scoped`
import Std.Tactic.Where
open scoped Nat
#where -- In root namespace with initial scope
Duplicate of https://github.com/leanprover-community/mathlib4/issues/12606 because I didn't realize #where is defined here.