Zulip Chat Archive

Stream: general

Topic: unreachable code

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

Mario Carneiro (Dec 12 2018 at 00:01):

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

Kenny Lau (Dec 12 2018 at 00:02):

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

Mario Carneiro (Dec 12 2018 at 00:02):

@Sebastian Ullrich known bug?

Sebastian Ullrich (Dec 12 2018 at 08:23):

Probably not. Probably not worth fixing, either?

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:

Simon Hudon (Dec 12 2018 at 15:25):

Oh dear!

Last updated: Dec 20 2023 at 11:08 UTC