Zulip Chat Archive

Stream: general

Topic: red squiggle in wrong place?


view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Jul 02 2020 at 11:34):

red.png

view this post on Zulip Mario Carneiro (Jul 02 2020 at 11:35):

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

view this post on Zulip Mario Carneiro (Jul 02 2020 at 11:35):

consider

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

view this post on Zulip 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