Unhelpful error message

Stream: mathlib4

[Michael Stoll]

import Mathlib.Tactic

example (n : Nat) : Nat :=
| 0 => 0 -- error "expected no space before" at `|`
| n + 1 => 2

(Without imports, it already errors at := with "unexpected token '|'; expected term", which I find more helpful.)

Is there syntax that makes this work? (I.e., with n left of the colon.)

[Yaël Dillies]

example (n : Nat) : Nat :=
  match n with
  | 0 => 0
  | n + 1 => 2

[Kyle Miller]

What's happening is that | is used for mathlib's absolute value notation as well, and to help prevent ambiguities that notation requires no whitespace after the first | and before the second | in |x|. The parser doesn't know that the | after the := shouldn't be the start of an absolute value expression.

[Michael Stoll]

The point is that there is no space before the |! Since the |has the red squiggle, the error messsage seems to say that Lean expects no space before the |, which is rather absurd in this case.

[Kyle Miller]

I don't disagree with you Michael. I'm explaining where the error is coming from because I spent a few minutes looking for what is causing it, and maybe someone will have energy to fix it.

[Kyle Miller]

I also spent a few minutes trying to see how to get the noWs parser to give a better error message here.

[Mario Carneiro]

IMO the noWs parser should highlight the whitespace and give an error like "expected no space here"

[Mario Carneiro]

of course it could also take an optional message for better results in specific contexts