Users may add the expensive instances if they want.
The goal is to make sure the default configuration is solid, and
covers all examples we really want to support.
cc @kha @dselsam
The main issue is nontermination for problems that do not have
solution. When using dependent coercions, we keep creating goals of
the form `CoeSort ... (coe (coe (coe ...))) ...`. Same for `CoeFun`.
I am considering simplifying it even further, and making sure
`CoeDep` can be used at most once in a sequence of coercions `CoeTC`.
Another option is to use a very small amount of fuel to
guarantee termination when solving coercion TC problems.
cc @Kha @dselsam
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
@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]
```
