What does open_locale do?

Stream: new members

[Jiang Jiedong]

Hi everyone!
I am reading some mathlib lean3 codes on GitHub and find many files includes lines like
open_locale classical big_operators
What does this line actually do? When do I need to include this in my lean project? Thanks!

[Ruben Van de Velde]

It provides the syntax described at https://leanprover-community.github.io/mathlib_docs/algebra/big_operators/basic.html

[Ruben Van de Velde]

If you need that syntax, you need to include the open_locale big_operators line

[Ruben Van de Velde]

open_locale classical does something so that you don't have to think about decidability anymore, but somehow you only end up thinking about it more