Commit 2022-08-30 11:08 3d7987cd

chore(*): bump to lean 3.47.0 (#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.