2231d9b488
This PR changes the way that scientific numerals are parsed in order to give better error messages for (invalid) syntax like `32.succ`. Example: ```lean4 #check 32.succ ``` Before, the error message is: ``` unexpected identifier; expected command ``` This is because `32.` parses as a complete float, and `#check 32.` parses as a complete command, so `succ` is being read as the start of a new command. With this change, the error message will move from the `succ` token to the `32` token (which isn't totally ideal from my perspective) but gives a less misleading error message and corresponding suggestion: ``` unexpected identifier after decimal point; consider parenthesizing the number ``` |
||
|---|---|---|
| .. | ||
| bench | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lakefile.toml | ||
| lean-toolchain | ||