notation/notation3

Stream: mathlib4

[Yury G. Kudryashov]

I started porting measure_theory.measurable_space_def. I tried to copy notation for IsOpen[t] to get notation for MeasurableSet[m],

set_option quotPrecheck false in
scoped[MeasureTheory] notation "measurable_set[" m "]" => @MeasurableSet _ m

and it seems that Lean tries to parse it as a notation3: the error message is

72:6:
expected 'binder_predicate', 'elab', 'elab_rules', 'infix', 'infixl', 'infixr', 'instance', 'macro', 'macro_rules', 'notation', 'notation3', 'postfix', 'prefix', 'syntax' or 'unif_hint'
72:58:
no macro or `[quot_precheck]` instance for syntax kind 'Lean.Parser.Term.explicit' found
  @MeasurableSet
This means we cannot eagerly check your notation/quotation for unbound identifiers; you can use `set_option quotPrecheck false` to disable this check.

and it shows help for notation3 when I hover the word "scoped".

[Yury G. Kudryashov]

I wonder why this doesn't happen with notation for IsOpen[t] but happens here.

[Reid Barton]

Does it work without scoped[MeasureTheory]?

[Reid Barton]

If it's in the MeasureTheory namespace already, you can also just write scoped

[Yury G. Kudryashov]

namespace MeasureTheory
set_option quotPrecheck false in
scoped notation "measurable_set[" m "]" => @MeasurableSet _ m

end MeasureTheory
open MeasureTheory

[Yury G. Kudryashov]

works

[Yury G. Kudryashov]

I'll use it as a workaround.