## Stream: new members

### Topic: Scoping notation

#### Eduardo Cavazos (Dec 09 2019 at 05:14):

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 (Dec 09 2019 at 05:17):

You can look into localized notation in mathlib

#### Eduardo Cavazos (Dec 09 2019 at 05:23):

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


Last updated: May 11 2021 at 12:15 UTC