pp_extended_field_notation

Stream: mathlib4

[Kyle Miller]

"Extended field notation" is the name for when you use x.f notation to mean Foo.f x, supposing you have x : Foo ... and some function Foo.f defined. Lean 4 recognizes extended field notation, but it does not pretty print using it.

There is now a command in the Mathlib.Tactic.ProjectionNotation module called pp_extended_field_notation to configure a function to be pretty printed using dot notation. Right now the syntax is simply pp_extended_field_notation Foo.f (and depending on namespaces you can often do pp_extended_field_notation f).

Rules:

• It should only be used on functions whose first explicit argument receives the object of the dot notation.
• It should not be used on functions of the form toFoo (anything that looks like a projection to a parent structure) since at the moment it might confuse other pp_extended_field_notation pretty printers.
• It may be used on true projections, which is useful if the projection can take additional arguments (for example, docs4#Prefunctor.obj takes both the Prefunctor and an additional value). The built-in Lean 4 dot notation pretty printer skips using dot notation in this case.

[Kyle Miller]

Another thing that might be useful is that by just importing Mathlib.Tactic.ProjectionNotation you get a special pretty printer that collapses parent projections, so rather than x.toC.toB.toA.f it comes out as x.f. You can turn this off using set_option pp.collapseStructureProjections false.

[Eric Wieser]

I assume you mean first explicit argument

[Kyle Miller]

Sure, it should only be used for cases of extended field notation where the first explicit argument is the receiver of the dot notation object.

[Kyle Miller]

Lean 4's dot notation passes the object to the first matching argument (explicit or not), and pp_extended_field_notation shouldn't be used in the non-explicit case.

[Peter Nelson]

It seems like this needs to be done in every new file for which the pretty-printed dot is wanted. Is there a way to enable it globally at the point where the declaration is made?

[Kyle Miller]

If you put it right after the corresponding declaration, it should be global

[Kyle Miller]

(Or more generally, if you import a file that uses pp_extended_field_notation on a declaration then you should see it work in the current module)

[Kyle Miller]

I just got around to making a more convenient way to apply pp_extended_field_notation: #5632

With this, instead you use the @[pp_dot] attribute. (RFC: Is this a fine name for the attribute?)