avoiding parentheses around notation

Stream: general

[Rémy Degenne]

I have the following notation definition, and I would like the first example to work.

import measure_theory.measurable_space_def

notation `measurable_set'` m := @measurable_set _ m

variables {α : Type*} {m : measurable_space α} {s : set α}

example (hs : @measurable_set _ m s) : measurable_set' m s := hs  -- error: function expected at m

example (hs : @measurable_set _ m s) : (measurable_set' m) s := hs -- works

The issue is that m s is understood to be the argument of the notation instead of m only. How can I change that behaviour?

[Rémy Degenne]

An alternative would be to define a notation taking two arguments, but I don't know how to do that without introducing a symbol between them:

notation `measurable_set'` m s := @measurable_set _ m s           -- error
notation `measurable_set'` m `,` s := @measurable_set _ m s   -- works, but not what I want

[Eric Wieser]

notation `measurable_set'` := @measurable_set _ seems to work

[Rémy Degenne]

Thanks! It works indeed.

[Eric Wieser]

notation `measurable_set'` m:max := @measurable_set _ m works too

[Eric Wieser]

Is there a reason for avoiding abbreviation here?

[Rémy Degenne]

Interesting. Do you have a link to documentation about that :max? I would like to know more

[Eric Wieser]

:max is just :1024

[Eric Wieser]

After all, there are no larger integers /s

[Rémy Degenne]

My dumb reason for not using abbreviation is that I don't know what it is. I'll look it up.

[Rémy Degenne]

Do you have a link to documentation about abbreviation?

[Eric Wieser]

No, but I can tell you that abbreviation is just short for @[inline, reducible] def, and you almost certainly don't care about inline.

[Eric Wieser]

attr#reducible isn't documented in a way doc-gen understands

[Rémy Degenne]

Thanks. Is there an advantage to using abbreviation instead of notation?

[Eric Wieser]

The main one I can think of is that it works with namespaces,measurable_space.measurable_set' would only work with abbreviation and not notation

[Kevin Buzzard]

This recent conversation cleared up a lot of my confusion about the difference between abbreviation and notation.

[Mario Carneiro]

I think you want this to be a notation and not an abbreviation, since it is being used as a shorthand to write statements involving measurable_set with unusual instances