How do I define equality for enum types?

Stream: new members

[Rui Liu]

I can define enum types like this

inductive weekday : Type
| sunday : weekday
| monday : weekday
| tuesday : weekday
| wednesday : weekday
| thursday : weekday
| friday : weekday
| saturday : weekday

However, ite (weekday.sunday = weekday.monday) 0 1 fails to reduce, complaining something like the equality is not decidable?

failed to synthesize type class instance for
⊢ decidable (weekday.sunday = weekday.monday)

How do I make the equality for enum types decidable?

[Kevin Buzzard]

Try putting @[derive decidable_eq] before inductive.

[Rui Liu]

That works!