Zulip Chat Archive

Stream: general

Topic: Disable notation?


Heather Macbeth (Aug 04 2022 at 20:28):

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 (Aug 04 2022 at 20:29):

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

Heather Macbeth (Aug 04 2022 at 20:30):

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

Kyle Miller (Aug 04 2022 at 20:30):

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

infixl ` × `:70 := has_mul.mul

works

Eric Rodriguez (Aug 04 2022 at 20:31):

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

Kyle Miller (Aug 04 2022 at 20:31):

set_option pp.notation false

Kevin Buzzard (Aug 04 2022 at 20:34):

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 (Aug 04 2022 at 20:39):

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


Last updated: Dec 20 2023 at 11:08 UTC