lean4
lean4 copied to clipboard
fix: bug in do expansion
As reported on zulip. The second commit fixes #2663, which looks similar but is a separate issue. I also fixed some typos and formatting issues in the debugging code in this file.
This change now causes an unreachable warning on the following code:
example := do
let x <- return
which is kind of true? But the error message points at the following doElem and says that is unreachable, which doesn't make much sense here since it points at the whole statement including the return. So I added a mechanism to suppress this error. (PS: this should really be a warning, not an error. The code is perfectly well interpretable even if parts of it are not reachable, and this can make editing annoying.)