Stream: new members
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
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 (Dec 10 2020 at 23:05):
@[derive decidable_eq] before
Rui Liu (Dec 10 2020 at 23:27):
Last updated: May 08 2021 at 03:17 UTC