Polynomial.eval dot-notation delaborator

Stream: mathlib4

[Johan Commelin]

Do I understand correctly that it is now possible to make Polynomial.eval x f pretty-print as f.eval x in the infoview. What is the code snippet that will enable this?
cc @Kyle Miller

[Junyan Xu]

When you say "now possible", do you mean it's due to the recent enablement of dot notation for bundled functions? But docs#Polynomial.eval has always been a plain function. I'd like to see dot notation used for docs#Polynomial.aeval though.

[Johan Commelin]

Aah, you are right. I forgot it was a plain function :man_facepalming:

[Edward van de Meent]

actually, lean4#6178 says that although the syntax is now allowed, the pp doesn't show it yet.

[Edward van de Meent]

(give the issue a thumbs up if you think this is important)