@Kha I am adding a few examples to use in the manual.
This one is a bit ugly due to two issues
1- We can't easily copy the position information from one token to
another. You suggested a notation in the past, but we never
implemented it. In the new example, we must copy the `end` position to
`}` to get the "unsolved goals" error message at the `end` token.
2- The quotation `` `(by { $ts* }) `` doesn't do what we want.
The issue is that we are using `group` instead of `nodeWithAntiquot`
to define `tacticSeqBracketed`. I will have to go over all parsers we
have defined, and check how many other places have this problem.
@Kha We are still accepting wildcard alternatives of the form
`| _ => ...`
It is useful when we can discharge many alternatives using the same
tactic, and it looks like the wildcard alternative used in "match"-expressions.
Before this commit, each `isDefEq u v` invocation would fail if there
were pending universe level constraints. This commit, moves the
postponed universe constraints back to the `MetaM` state.
It also adds the combinator
```lean
withoutPostponingUniverseConstraints x
```
which executes `x` and throws an error if there are pending universe
constraints. We use the combinator at `elabApp` and `elabBinders`.
Without this commit, we would fail to elaborate simple terms such as
```lean
Functor.map Prod.fst (x s)
```
because after elaborating `Prod.fst` and trying to ensure its type
match the expected one, we would be stuck at the universe constraint:
```
u =?= max u ?v
```
Another benefit of the new approach is better error messages. Instead
of getting a mysterious type mismatch constraint, we get a list of
universe contraints the system is stuck at.
cc @Kha
