Zulip Chat Archive

Stream: general

Topic: unreachable code


view this post on Zulip Kenny Lau (Dec 12 2018 at 00:00):

sometimes _ causes "unreachable code" error. it is quite clear that they won't fix it, so I'm not here to "feed the fed horse". Rather, I think I've found a temporary fix by just replacing _ with by skip or any tactic mode thing at all

view this post on Zulip Mario Carneiro (Dec 12 2018 at 00:01):

That's a bit vague. Do you have an example?

view this post on Zulip Kenny Lau (Dec 12 2018 at 00:02):

instance : group ( × ) :=
{ mul := λ _ _, (_, _) }

view this post on Zulip Mario Carneiro (Dec 12 2018 at 00:02):

@Sebastian Ullrich known bug?

view this post on Zulip Sebastian Ullrich (Dec 12 2018 at 08:23):

Probably not. Probably not worth fixing, either?

view this post on Zulip Sebastian Ullrich (Dec 12 2018 at 08:24):

To be honest, the Lean 4 error messages are so bad right now that I don't see any problem at all with this :laughing:

view this post on Zulip Simon Hudon (Dec 12 2018 at 15:25):

Oh dear!


Last updated: May 16 2021 at 21:11 UTC