notation vs notation3

Stream: mathlib4

[Johan Commelin]

rg '^scoped.*notation ' | wc -l
146

Should all of these be updated to notation3 to give them a delaborator?

cc @Kyle Miller

[Kyle Miller]

Whether there is a delaborator is a matter of what's on the RHS of the =>. I think both notation and notation3 support scoped.

The built-in notation command is able to make a delaborator if the RHS is just an application like f x y z, but if you use more complicated syntax it gives up making a delaborator. The notation3 command has a more sophisticated delaborator generator, and it gives you a warning when it's given up.

I wouldn't change notation to notation3 unless you notice something isn't pretty printing, and you know it's notation that you do want to pretty print.

[Kyle Miller]

The notation example over at https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/.28infinity.2C.201.29-categories/near/410554558 probably failed to make a delaborator because of the type ascription.

[Kyle Miller]

(I think eventually either (1) the core notation command will have a more comprehensive delaborator generator, (2) we'll rename notation3 to something that doesn't suggest it's just a mathport command, or (3) maybe both?)

[Johan Commelin]

Ok, then I will not make a sweeping change for now.