issue !4#11180: Porting note: removed `@[pp_nodot]`

Stream: triage

[Random Issue Bot]

Today I chose issue 11180 for discussion!

Porting note: removed @[pp_nodot]
Created by @Pietro Monticone (@pitmonticone) on 2024-03-05
Labels: porting-notes

Is this issue still relevant? Any recent updates? Anyone making progress?

[Kyle Miller]

Now that we have general pretty printing of dot notation and @[pp_nodot] in 4.8.0, #13781 goes through the @[pp_nodot] porting notes.

There are some places mathlib3 had @[pp_nodot] that never could have had an affect (dot notation would never have been used), in which case I deleted the porting note. There are also some places that currently dot notation won't be used, but conceivably lean4#1910 could enable dot notation at some point in the future, so I added @[pp_nodot] and modified the porting note.