This allows efficient recovery from a parse error as well as implementing `has_to_string` for `message` |
||
|---|---|---|
| .. | ||
| basic.lean | ||
| module.lean | ||
| term.lean | ||
| token.lean | ||
This allows efficient recovery from a parse error as well as implementing `has_to_string` for `message` |
||
|---|---|---|
| .. | ||
| basic.lean | ||
| module.lean | ||
| term.lean | ||
| token.lean | ||