Notation error for norm

Stream: mathlib4

[Anatole Dedecker]

Is there a good reason for the following to fail?

import Mathlib.Analysis.NormedSpace.Basic

example (x : ℝ) : ‖x ‖ = 0 := sorry -- expected term

[Jireh Loreaux]

I guess for human parsing (and maybe Lean too?) it's helpful if there is no space between the norm symbols and the stuff inside it.

[Anatole Dedecker]

Well it's definitely cleaner, but this is really annoying for beginners who don't have this kind of style rules in mind.

[Jireh Loreaux]

fair point. Is \norm a valid abbreviation in the Lean 4 extension yet? (EDIT: seems not, that would have helped with cursor placement)

[Anatole Dedecker]

I think it is :thinking:

[Jireh Loreaux]

Lol, I have a very old version of lean-m17n that was hijacking the Lean 4 extension and not doing the replacement.

[Patrick Massot]

I guess this is the price to pay for having a reasonable notation. Here, as often, reasonable means the same token is a delimiter on both sides.

[Kevin Buzzard]

AKA "unreasonable", as far as some computer scientists are concerned :-)

[Patrick Massot]

I know, hence my emphasis.

[Sebastian Ullrich]

There is workable syntax, and then there is workaroundable syntax