Disable notation?

Stream: general

[Heather Macbeth]

For a talk, I'd like to disable the notation * for has_mul.mul and instead use the notation ×. Is there a way to locally disable a single notation? Unfortunately the * notation is defined all the way back in core Lean, so I can't even achieve what I want by making my own custom version of mathlib.

[Yaël Dillies]

Can you not define × as notation for has_mul.mul with higher priority than *?

[Heather Macbeth]

Ah, priorities. Yes, this seems to work. Thanks!

[Kyle Miller]

It appears that it doesn't need to even be higher priority,

infixl ` × `:70 := has_mul.mul

works

[Eric Rodriguez]

Turning off notation fully has other uses too, such as debugging. I asked for this recently; is it possible at all?

[Kyle Miller]

set_option pp.notation false

[Kevin Buzzard]

IIRC Eric wanted to just turn one piece of notation off, and didn't get any answers about how to do it (but I might be confusing his question with another question)

[Eric Rodriguez]

yeah because if you do that you get goals such as @eq (@has_mul.mul ...) when I just want to see the implicits for one piece of notation