7b813622c6
@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. |
||
|---|---|---|
| .. | ||
| Delaborator | ||
| Basic.lean | ||
| Delaborator.lean | ||
| Formatter.lean | ||
| Parenthesizer.lean | ||