# Zulip Chat Archive

## Stream: new members

### Topic: match statement in decidable instance

#### Chris B (Jul 19 2019 at 02:53):

Does anyone know what the `decidable_eq ℕ`

instance in core does that allows it to use the syntax `match decidable_eq x y with ...`

in the recursive case? Trying to use it elsewhere gives me an error.

inductive not_nat | Z : not_nat | S : not_nat → not_nat open not_nat instance : decidable_eq not_nat | Z Z := is_true rfl | (S x) Z := is_false (λ h, not_nat.no_confusion h) | Z (S y) := is_false (λ h, not_nat.no_confusion h) | (S x) (S y) := match decidable_eq x y with -- ... -- type mismatch at application -- decidable_eq x -- term -- x -- has type -- not_nat : Type -- but is expected to have type -- Sort ? : Type ?

#### Mario Carneiro (Jul 19 2019 at 02:55):

If you look at the tactic state in the error message, you will see that `not_nat.decidable_eq`

is what's in the context, so you have to write it like that

#### Mario Carneiro (Jul 19 2019 at 02:56):

It's not actually a global definition, it's actually a local constant in disguise (and actually it's not even that, it's a macro disguised as a local constant) so it doesn't work by the same rules w.r.t `open`

#### Mario Carneiro (Jul 19 2019 at 02:58):

The difference between your example and `nat.decidable_eq`

is that `nat.decidable_eq`

was written inside `namespace nat`

rather than merely with `nat`

open

#### Mario Carneiro (Jul 19 2019 at 02:58):

this works:

inductive not_nat | Z : not_nat | S : not_nat → not_nat namespace not_nat instance : decidable_eq not_nat | Z Z := is_true rfl | (S x) Z := is_false (λ h, not_nat.no_confusion h) | Z (S y) := is_false (λ h, not_nat.no_confusion h) | (S x) (S y) := match decidable_eq x y with | _ := sorry end end not_nat

#### Chris B (Jul 19 2019 at 03:01):

Agh, brutal. I tried some of the qualifiers but definitely not namespace. I'm still trying to get a grasp on how the hierarchical names work in practice. Thanks for the rundown.

#### Mario Carneiro (Jul 19 2019 at 03:02):

I think this is actually more like a bug in the way instance names and auxiliaries are handled, so I don't blame you for getting confused

Last updated: May 14 2021 at 03:27 UTC