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):
instance : decidable_eq my_type := by mk_dec_eq_instance
Mario Carneiro (Jun 20 2018 at 18:49):
Last updated: May 10 2021 at 19:16 UTC