feat: allow explicit mode with field notation

[kmill]

Now one can write @x.f, @(x).f, @x.1, @(x).1, and so on.

This fixes an issue where structure instance update notation (like {x with a := a'}) could fail if the field a had a type with implicit, optional, or auto parameters.

Closes #5406

[leanprover-community-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-5528 build failed against this PR. (2024-09-30 01:49:24) View Log
• ✅ Mathlib branch lean-pr-testing-5528 has successfully built against this PR. (2024-10-09 07:32:00) View Log

[digama0]

isn't this ambiguous? If x : {a : A} -> Foo a and Foo.f {a' : A} : Foo a' -> {b : B} -> R, does @x.f introduce a or a'/b as explicit?

[kmill]

@digama0 The current precedence rules have @x.f parse as @ applied to x.f. Same for @(x).f, it's @ applied to (x).f. On the other hand, (@x).f is @ applied to x.

Dot notation doesn't work when x is a function, so (@x).f isn't useful as an interpretation.

[alreadydone]

Dot notation doesn't work when x is a function

What do you mean? (web editor)

import Mathlib.Logic.Function.Defs
variable {α β} (f : α → β)
#check f.Injective

[kmill]

@alreadydone Discussion about that here