Zulip Chat Archive
Stream: general
Topic: auto deriving decidable
Zesen Qian (Jun 20 2018 at 17:53):
Is there some way to derive decidable instance from a inductive definition?
Zesen Qian (Jun 20 2018 at 17:56):
sorry, I mean the decidable instance for equality on this inductive type.
Simon Hudon (Jun 20 2018 at 17:57):
Try:
instance : decidable_eq my_type := by mk_dec_eq_instance
Mario Carneiro (Jun 20 2018 at 18:49):
or @[derive decidable_eq]
Last updated: May 02 2025 at 03:31 UTC