Stream: general

Topic: red squiggle in wrong place?

Kevin Buzzard (Jul 02 2020 at 11:32):

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?

red.png

Mario Carneiro (Jul 02 2020 at 11:35):

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

Mario Carneiro (Jul 02 2020 at 11:35):

consider

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


Mario Carneiro (Jul 02 2020 at 11:37):

but it does seem to be unique to type ascriptions

Last updated: May 11 2021 at 00:31 UTC