@Kha this is a fix for the example that @gebner posted on Zulip.
There are other possible workarounds, but I think this one is
"intuitive".
Here is the problem description and workaround.
We currently use the `withPosition` combinator at `matchAlts`. The
original motivation was nested `match`-expressions without
parenthesis.
We also have the `checkColGt` in the application parser.
Thus, `frob 5` is not parsed as an application. That is, the term
parser after the `then` keyword stops at `frob`.
Then, we get the weird "expected 'else'" error message at `5` :)
In this commit, I add a `checkColGe` check at the beginning of each
alternative right-hand-side.
The effect on the stdlib was minimal. It basically affected old code
that used the Lean 3 workaround for partial functions
```
partial def f : N -> N | i =>
...
```
In Lean 4, we can use the more natural
```
partial def f (i : N) : N :=
...
```
or
```
partial def f : N -> N := fun i =>
...
```
It also affected code such as
```
instance : Repr String.Iterator where
reprPrec | ⟨s, pos⟩, prec =>
Repr.addAppParen ("String.Iterator.mk " ++ reprArg s ++ " " ++ reprArg pos) prec
```
This is a workaround for a missing feature. We really wanted to write
```
instance : Repr String.Iterator where
reprPrec ⟨s, pos⟩ prec :=
Repr.addAppParen ("String.Iterator.mk " ++ reprArg s ++ " " ++ reprArg pos) prec
```
@Kha I marked the corresponding methods as `protected`.
I currently can't stand `throw_error`, and I am optimistic about
server highlighting feature you are working on :)
@Kha It felt odd that we can write
```
map f x := ...
```
in instances, but we had to write
```
map (f x) := ...
```
when setting the field default value in a class.
@Kha Now, all parsers defined by `Init/Std/Lean` packages have
precedence >= `min` and <= `max`.
The only exception is `<|>` since it is an infix operator sharead with
the tactic DSL.
BTW, the meaning of `f $ a <|> b` changed with this commit.
It was `f (a <|> b)`, and now is `(f a) <|> b`. The problem is that
the precedence of the `$` parser is now greater than the `<|>` parser.
I will try another experiment where I make sure we do not "reuse"
term infix operators in the tactic DSL.
