List notation is broken by conditional probability

Stream: mathlib4

[Eric Wieser]

import Mathlib

open scoped ProbabilityTheory

theorem help : Nat.ofDigits 10 [0, 1] = 10 := rfl -- syntax error

[Eric Wieser]

This is caused by notations like

/-- The conditional probability measure of measure `μ` on set `{ω | X ω = x}`.

It is `μ` restricted to `{ω | X ω = x}` and scaled by the inverse of `μ {ω | X ω = x}`
(to make it a probability measure): `(μ {ω | X ω = x})⁻¹ • μ.restrict {ω | X ω = x}`. -/
scoped notation:max μ "[" s " | "  X " in " t "]" => μ[s | X ⁻¹' t]

[Eric Wieser]

#22699 has a fix, but it loses all the delaborators

[Eric Wieser]

@Kyle Miller, could notation or notation3 be taught to accept noWs?

[Eric Wieser]

(deleted)

[Eric Wieser]

cc @Yaël Dillies for #18663

[Eric Wieser]

Oh whoops, I forgot to open the scope for that one, sorry

[Eric Wieser]

Eric Wieser said:

#22699 has a fix, but it loses all the delaborators

I've added back the delaborators now.

[Kyle Miller]

Eric Wieser said:

Kyle Miller, could notation or notation3 be taught to accept noWs?

I think so, but it might take re-imagining how they work to some degree.

By the way, in your PR, it looks like you can use an app unexpander for everything but DFunLike.coe. App unexpanders are nice because they look like the inverse of the macro. (notation defines app unexpanders)

[Eric Wieser]

Done, thanks for the reminder than unexpanders exist

[Eric Wieser]

Would it be possible for errors like "expected |" to appear as "expected | (from parser Foo.bar and Bar.baz)" to make this kind of trap easier to track down in future

[Edward van de Meent]

or at least an option to enable this kind of debug message

[Aaron Liu]

Eric Wieser said:

Would it be possible for errors like "expected |" to appear as "expected | (from parser Foo.bar and Bar.baz)" to make this kind of trap easier to track down in future

the code is docs#Lean.Parser.Error.toString