Scoping notation

Stream: new members

[Eduardo Cavazos]

Chapter 7 mentions how to implement list. Instead of reusing the identifier list, I used List:

namespace hidden_72

universe u

inductive List (α : Type u)
| Nil {} : List
| Cons : α → List → List

open List

notation `[` l : (foldr `,` (h t, Cons h t) Nil) `]` := l

#check [1, 2, 3, 4, 5] -- [1,2,3,4,5] : List ℕ

end hidden_72

In a later namespace, I was surprised to see that the [ ] notation carried over:

namespace hidden_73

#check [10, 20, 30] -- [10,20,30] : hidden_72.List ℕ

end hidden_73

Is there a way to limit the scope of the custom [ ] notation on my List to just namespace hidden_72?

I.e. in any later separate namespace after hidden_72, I'd like for the [ ] notation to build a list, not a List.

Thanks!

[Simon Hudon]

You can look into localized notation in mathlib

[Eduardo Cavazos]

You can look into localized notation in mathlib

Interesting! Thanks @Simon Hudon!

For anyone curious, the above example converted to use localized looks as follows:

import tactic.localized

namespace hidden_72

universe u

inductive List (α : Type u)
| Nil {} : List
| Cons : α → List → List

open List

localized "notation `[` l : (foldr `,` (h t, Cons h t) Nil) `]` := l" in my.List

#check [1, 2, 3, 4, 5] -- [1,2,3,4,5] : List ℕ

end hidden_72


namespace hidden_73

#check [10, 20, 30] -- list ℕ

end hidden_73