open scoped

Stream: new members

[Kevin Buzzard]

From Mathlib.Algebra.Quaternion:

The following notation is available with `open Quaternion` or `open scoped Quaternion`.

* `ℍ[R, c₁, c₂]` : `QuaternionAlgebra R c₁ c₂`
* `ℍ[R]` : quaternions over `R`.

What's the difference between open and open scoped?

[Damiano Testa]

I think that open scoped does a subset of what open does: it "opens" what is in

scoped[AddMonoidAlgebra] notation:9000 R:max "[" A "]" => AddMonoidAlgebra R A

but does not also give you access to the AddMonoidAlgebra. lemmas without the AddMonoidAlgebra-prefix.

[Damiano Testa]

import Mathlib

open scoped Polynomial

#check Nat[X]
#check C  -- fails

open Polynomial

#check Nat[X]
#check C

[Damiano Testa]

The notation Nat[X] works the first time, since it is scoped, but C is not picked up as Polynomial.C.

[Kevin Buzzard]

Oh -- is it like lean 3 open locale?

[Damiano Testa]

Ah, very likely yes! Maybe not literally, but probably close enough.

[Kevin Buzzard]

Lean 4 open = Lean 3 open + open locale (i.e. the namespace plus the notation), and Lean 4 open scoped is just the notation but not the namespace?

[Damiano Testa]

Yes, at least this is my mental model. With some flexibility about possible edge cases. I think that also instances can be scoped.

[Michael Stoll]

Yes, they can.

[Damiano Testa]

I think that open_locale also allowed instances anyway, so probably the analogy with open_locale is quite accurate.

[Floris van Doorn]

Yes, open scoped is indeed the analogue of open_locale in Lean 3. Except in Lean 3 it was a hack, and Lean 4 supports it natively.

[Floris van Doorn]

And in both versions you could scope/localize any attribute (including instances) and notation.

[Floris van Doorn]

In Lean 4 you can also scope things like macros, pretty printers, parsers, and various other things.

[Floris van Doorn]

e.g. we now have notation ∑ (x ∈ s) (y ∈ s), f x y and we could imagine writing a pretty printer for that. But because it obscures what is going on, that maybe should be a scoped pretty printer

[Eric Wieser]

One thing that's missing here is an open notscoped Foo that matches the behavior of the lean 3 open foo. (for Nat, it would put factorial in the local environment, but not the ! notation)

[Eric Wieser]

Maybe it could be spelt open Nat (*), which matches open Nat (factorial)

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Eric Wieser said:

One thing that's missing here is an open notscoped Foo that matches the behavior of the lean 3 open foo. (for Nat, it would put factorial in the local environment, but not the ! notation)

For this reason I have been writing

namespace Foo
namespace Notation
...
end Notation
...
end Foo

so that open Foo does not necessarily bring in the notation.