binding scopes to notations?

Stream: lean4

[Jason Gross]

Is there a way to bind notations to scopes? Said another way, is there a way to use the same notation for two different things, and then disambiguate between them post-hoc?

[Leonardo de Moura]

In Lean, we have "scoped" and "local" attributes. You can use them for notation, instances, unification hints, simp lemmas, etc.
It is not documented yet, but here is an example.
https://github.com/leanprover/lean4/blob/f000aa0155f9ec168a017931631409e0125eecc6/tests/lean/run/scopedParsers2.lean

[Leonardo de Moura]

namespace Foo

  def f (x y : Bool) := x || y

  scoped infix:65 "++" => f

  #check true ++ false -- Ok

end Foo

#check true ++ false -- Error

section
  open Foo
  #check true ++ false -- Ok
end

-- The following doesn't work yet because we parse the command before we (elaborate it and) open the namespace
#check (open Foo in true ++ false)

[Jason Gross]

Neat, thanks! Are you planning to fix the open Foo in ... example? I think it would be quite useful

[Leonardo de Moura]

Jason Gross said:

Neat, thanks! Are you planning to fix the open Foo in ... example? I think it would be quite useful

Yes, we are planning to do it. This one and local notations are on our to-do list, just not a high priority right now :)