What does open_locale do?

Stream: general

[YH]

I just saw this in mathlib

[Reid Barton]

https://github.com/leanprover-community/mathlib/blob/master/docs/tactics.md#localized-notation

[YH]

https://github.com/leanprover-community/mathlib/blob/master/docs/tactics.md#localized-notation

Thanks

[Bernd Losert]

Can someone explain or point me to an explanation of open_locale?

[Anne Baanen]

Here's the new link: https://leanprover-community.github.io/mathlib_docs/commands.html#localized%20notation

[Bernd Losert]

Thanks. I did not realize it was a mathlib thing. I thought it was a lean builtin.