batteries icon indicating copy to clipboard operation
batteries copied to clipboard

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

Open fpvandoorn opened this issue 1 year ago • 0 comments

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.

fpvandoorn avatar May 02 '24 17:05 fpvandoorn