## 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