error position

Stream: lean4

[Jakob von Raumer]

In this snippet, I would expect the error to be in the first, third, or fourth line, but it appears in the second:

example : 5 = 3 :=
  have t : True := _
  have f : 5 = 6 := _
  f

Is this an issue with the language server or with the syntax position the error is thrown at?

[Mario Carneiro]

Also, it highlights the entire span have t : True := _. Errors with large span should generally be avoided because they tend to obscure other errors in nested spans. (I say this having written a language server that made exactly this mistake. An error covering your entire definition is very distracting.) exact also has a problem with large span errors