We can now write
```lean
syntax "case!" ident ":" term "with" term "," term : term
macro_rules
| `(case! $h : $c with $t, $e) => `(let $h := $c; cond $h $t $e)
```
Before the series of commits to change `let` syntax, the
quasiquotation `(let $h := $c; cond $h $t $e)
produced the weird error message "`;` expected" at ":=".
The problem was that $h was matching the now deleted "nonterminal"
```lean
def letIdDecl := parser! try (letIdLhs >> " := ") >> termParser
```
This was not a bug, but a side-effect on how the `let` syntax was
declared.
cc @kha
It avoids hidden nonterminals, and store the equation case as a
separate rule. It would be great if we could have 3 independent rules,
but this is not possible because `longestMatch` would return a choice
for terms as simple as `let x := v; ...` The problem is that it is
both a `letSimpleDecl` and a `letPatDecl`. We resolve the ambiguity at
the parsing level using `<|>`.
cc @Kha
@Kha this commit fix another example of weird error message I have
experienced in the last few days.
The macro
```lean
syntax "case!" ident ":" term "with" term "," term : term
macro_rules
| `(case! $h : $cond with $t, $e) =>
`((fun $h => cond $h $t $e) $cond)
```
is accepted, but as in `fun` binders, we get a weird error when
trying to elaborate an instance of the macro.
Example:
```lean
check case! h : 0 == 0 with h, not h
```
@Kha I am adding this kind of feature to improve the user experience.
For example, the macro
```
syntax "[" ident "↦" term "]" : term
macro_rules
| `([$x ↦ $v]) => `(fun $x => $v)
```
is accepted and looks perfectly reasonable.
However, before this commit, we would get a nasty error when
elaborating
```lean
check [x ↦ x + 1]
```
@cipher1024 I modified your fix. It would produce memory leaks if the
code executed by #eval modifies the stdout.
Here is the problem.
- Your replaces the handler with some new handler `H` and stores the
old handler `O` in a `flet`.
- Code is executed and replaces the stdout handler with `H'`. The `H`s RC is
decremented and `H'`s RC is incremeneted. So far, so good.
- Now, the destructor of your `flet` is executed, and it replaces `H'`
with `O`, but `H'` RC is not decremented.
@Kha I added this feature to help debugging macros.
I was using `set_option trace.Elab true` as a workaround, but it is
too verbose.
For example, in the following buggy code
```
new_frontend
macro "foo" x:term : term => `(x + 1)
macro "bla" x:term : term => `(foo $x)
```
We get the error message
```
<input>:6:11: error: unknown identifier 'x.15'
with resulting expansion
x + 1
while expanding
foo 1
while expanding
bla 1
```
Perhaps we should preserve the macroscopes at "with resulting
expansion". Anyway, I think it is better than the previous error.
```
<input>:6:11: error: unknown identifier 'x.15'
while expanding
foo 1
while expanding
bla 1
```
