change in local notation?

Stream: general

[Thorsten Altenkirch]

Sorry I am still using lean 3 but it seems that there are different versions which differ in how they treat "local notation" (Actually how can I find out which version I am using?).
For my course I redefined the boolean connectives band and bor, because I don't like the braindead way they are defined in the core library. I introduced a namespace and defined:

local notation x && y := band x y
local notation x || y := bor x y

This worked but now on some installations it returns an error. :-(
Is there a way to fix this?

[Johan Commelin]

#eval lean.version should tell you the version you are using

[Johan Commelin]

Which error do you get?

[Thorsten Altenkirch]

I actually stupidly used my desktop to prepare the lecture and then my laptop for life proving and got caught by this issue in class? :-(

[Thorsten Altenkirch]

invalid notation: notation already declared. Consider using 'notation (name := ...)'

[Thorsten Altenkirch]

Ok it doesn't work on:
(3, (48, 0))

[Johan Commelin]

https://leanprover.zulipchat.com/#narrow/stream/116290-rss/topic/Recent.20Commits.20to.20mathlib.3Amaster/near/296106859 is biting you.

[Johan Commelin]

This is a backport from Lean 4 afaict.

[Thorsten Altenkirch]

rss-bot said:

chore(*): bump to lean 3.47.0 (mathlib#16252)

A major change is that notations now require names when they are shadowing another identical notation, even if it is a local notation. Also, because localized notations can be imported in a variety of contexts, there are some new best practices for them:

• localized notations should always have a (name := ...). Notation names are unrelated to declaration names, but the declaration name is a reasonable base for the notation name.
• localized notations should never use _ in the notation, because this gets desugared to a unique metavariable index, meaning that the notation will not be recognized as a duplicate of itself if open_locale is used when the notation is already available. Instead, you should use the hole! notation, which unfolds to _.

Another major change is that projection notation (x.foo) now always instantiates implicit arguments with metavariables, which is consistent with Lean 4. To simulate the older behavior, one can use either strict implicit arguments for the structure field (e.g. ∀ {{n}}, p n instead of ∀ {n}, p n) or, depending on specifics, writing λ _, x.foo to ensure the implicit argument is preserved as an argument.

Co-authored-by: Kyle Miller <kmill31415@gmail.com>

Authored-by: digama0 (commit)

[Thorsten Altenkirch]

How do I fix the error I get when declaring:

local notation x && y := band x y
local notation x || y := bor x y

to locally redefine && and || ?

rss-bot said:

chore(*): bump to lean 3.47.0 (mathlib#16252)

A major change is that notations now require names when they are shadowing another identical notation, even if it is a local notation. Also, because localized notations can be imported in a variety of contexts, there are some new best practices for them:

• localized notations should always have a (name := ...). Notation names are unrelated to declaration names, but the declaration name is a reasonable base for the notation name.
• localized notations should never use _ in the notation, because this gets desugared to a unique metavariable index, meaning that the notation will not be recognized as a duplicate of itself if open_locale is used when the notation is already available. Instead, you should use the hole! notation, which unfolds to _.

Another major change is that projection notation (x.foo) now always instantiates implicit arguments with metavariables, which is consistent with Lean 4. To simulate the older behavior, one can use either strict implicit arguments for the structure field (e.g. ∀ {{n}}, p n instead of ∀ {n}, p n) or, depending on specifics, writing λ _, x.foo to ensure the implicit argument is preserved as an argument.

Co-authored-by: Kyle Miller <kmill31415@gmail.com>

Authored-by: digama0 (commit)

[Thorsten Altenkirch]

So is there a workaround?

[Johan Commelin]

Can't you just do what the error suggests?

[Patrick Massot]

Thorsten Altenkirch said:

I actually stupidly used my desktop to prepare the lecture and then my laptop for life proving and got caught by this issue in class? :-(

To me using a different version of Lean when preparing and when lecturing seems more "braindead" than the definition of band and bor in core Lean.

[Mario Carneiro]

Like johan and the error message say, the fix is to declare a name for the notation, it can be anything you like:

local notation (name := foo) x && y := band x y
local notation (name := bar) x || y := bor x y