lean4 icon indicating copy to clipboard operation
lean4 copied to clipboard

fix: bug in do expansion

Open digama0 opened this issue 2 years ago • 0 comments

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.)

digama0 avatar Oct 12 '23 13:10 digama0