Decidable equality (finite)

Stream: new members

[Bjørn Kjos-Hanssen]

The following has an error due to failed to synthesize type class instance for x y : worlds ⊢ decidable (x = worlds.w0). How to fix... should I make equality decidable somehow? The intention is for the type worlds to be a finite set, such as {w0,w1,w2}.

inductive worlds : Type
| w0
| w1
| w2
def R : worlds → worlds → Prop := -- accessibility relation
    assume x, assume y,
    if x=worlds.w0 then
        if y=worlds.w0 then true else false
   else false

[Kevin Buzzard]

There will be some magic words, something like @[derive decidable_eq] which you can put just in front of inductive. I'm not at a computer but maybe searching this site for such incantations will help

[Bjørn Kjos-Hanssen]

Thanks @Kevin Buzzard, that did it!