Attribute `pp_nodot`

Stream: mathlib4

[Moritz Doll]

Does pp_nodot exist in Lean 4? Searching here, in mathlib 4 and the docs did not give any results, but it is also not in the tactics issue (or documented on the attribute page for mathlib 3 for that matter)

[Scott Morrison]

Probably not. We added that in Lean3 community edition long after Lean 4 "forked".

[Scott Morrison]

I guess it is important to have. I doubt this is something we can do from outside Lean 4, so unless someone tells us otherwise, this will need a Lean 4 issue.

[Yury G. Kudryashov]

Any updates?

[Mario Carneiro]

Kyle implemented this as a command

[Mario Carneiro]

pp_extended_field_notation

[Mario Carneiro]

but note that the polarity is reversed: you have to opt in not out

[Yury G. Kudryashov]

Indeed, I see that Lean doesn't print arsinh x as x.arsinh without any attrs.

[Kyle Miller]

I was planning on adding an attribute version too. Any suggestions for naming? One option is just @[pp_dot]. I was also thinking of an attribute on structures to ensure dot notation pretty prints for every field (function-valued fields generally fail to pretty print)