## 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: May 16 2021 at 21:11 UTC