```lean
match x : t with
| ...
```
Two possible intepretations for `x : t`:
1- The discriminant `t` where `x` is the name for the equality proofs `t = ...` in each alternative.
2- The discriminant `x` with a expected type `t` (aka motive) for the match.
This commit resolves the ambiguity by forcing no space before `:` in
the first interpretation.
cc @Kha
Several combinators (e.g., `checkNoWsBefore`) access the "leading
term" by retrieving the element on the top of the syntax stack.
However, the `longestMatchFn` was accumulating successful matches on
the syntax stack too. This commit makes sure the `longestMatchFn`
always push the "leading term" before trying a parser.
This commit also eliminates the `orelseFn` hack at `trailingLoopStep`.
Now, we use `longestMatchFn` for all parsers. Note that we have to add
a new combinator (`checkWsBeforeIfSymbol`) to make sure that `a[i]`
cannot be parsed by the `app` parsing rule.
Before removing the hack from `trailingLoopStep`,
`a[i]` was correctly parsed as an `arrayRef`. After the change,
the `app` parser is tried and it succeeds (IF we don't use
`checkWsBeforeIfSymbol`). It is an application using the list literal
`[i]`.
The `checkWsBeforeIfSymbol` ensures that `a[i]` is not a valid `app`.
cc @Kha
@Kha
I kept `TokenInfo` as is. That is, the `lbp` field is still `Option Nat`.
I changed my mind because we have the combinator `NonReservedSymbol`.
It feels weird to have a combinator that does not create a keyword,
but sets the `lbp`. Recall that it is used at `Lean/Parser/Tactic.lean`.
Other observations:
- We use symbols in auxiliary constructions (e.g., `mkAntiquot`). It
feels weird to set their `lbp` there.
- It felt weird to specify the `lbp` in places such as
```
def structCtor := parser! ident >> optional inferMod >> symbol " :: " 67
```
- We have a few parsing rules where the same symbol appears twice.
It is funny to set the `lbp` twice. Note that the approach we
discussed yesterday (retrieving the `lbp` from the `Environment`)
would not work here.
