Suppress warning @[pp_dot]

Stream: general

[Martin Dvořák]

How can I suppress the warning on @[pp_dot] or replace @[pp_dot] entirely?
I use it on Function.foo and Subtype.foo because the delaborator does not use the dot notation automatically there.

"The @[pp_dot] attribute is deprecated now that dot notation is the default with the introduction of pp.fieldNotation.generalized in Lean v4.8.0."

[Kyle Miller]

Options:

• Copy the pp_dot code into your own project, rename the option.
• Make app unexpanders for these functions. This is what pp_dot does for you.
• Give examples of the functions you need, maybe the Lean pretty printer can accommodate them at some point in the future.
• Ignore the warning, and hope that some upcoming Lean features to control dot notation might help avoid the need of pp_dot