## Stream: lean4

### Topic: binding scopes to notations?

#### Jason Gross (Mar 11 2021 at 20:08):

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 (Mar 11 2021 at 20:21):

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 (Mar 11 2021 at 20:26):

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 (Mar 11 2021 at 20:36):

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

#### Leonardo de Moura (Mar 11 2021 at 20:38):

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 :)

Last updated: May 07 2021 at 12:15 UTC