red squiggle in wrong place?

Stream: general

[Kevin Buzzard]

example : ℕ := (_ : ℕ)

Should the red underline be on the underscore or on the bracket? For me it's on the bracket. Kenny told me this was well-known. Is it an issue?

[Kevin Buzzard]

red.png

[Mario Carneiro]

It's not misplaced, lean is putting it exactly where it intended to

[Mario Carneiro]

consider

example : ℕ := ( ( _ : ℕ) : ℕ)
--             ^

[Mario Carneiro]

but it does seem to be unique to type ascriptions