Zulip Chat Archive

Stream: new members

Topic: How do I define equality for enum types?


view this post on Zulip Rui Liu (Dec 10 2020 at 23:03):

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?

view this post on Zulip Kevin Buzzard (Dec 10 2020 at 23:05):

Try putting @[derive decidable_eq] before inductive.

view this post on Zulip Rui Liu (Dec 10 2020 at 23:27):

That works!


Last updated: May 08 2021 at 03:17 UTC