Zulip Chat Archive

Stream: general

Topic: auto deriving instances


view this post on Zulip Zesen Qian (Jun 07 2018 at 01:20):

Is there a quick way to derive instances for type definitions like def boolean : Type := bool?

view this post on Zulip Kenny Lau (Jun 07 2018 at 01:20):

don't use them :)

view this post on Zulip Zesen Qian (Jun 07 2018 at 01:22):

I feel type synonym is useful in development.

view this post on Zulip Kenny Lau (Jun 07 2018 at 01:23):

pretty sure you can't find it anywhere in mathlib

view this post on Zulip Simon Hudon (Jun 07 2018 at 01:24):

If you mark your definition as reducible, I think, the instances will simply be inherited

view this post on Zulip Simon Hudon (Jun 07 2018 at 01:25):

Otherwise, you can do

instance : my_class some_synonym :=
by dsimp [some_synonym] ; apply_instance

view this post on Zulip Zesen Qian (Jun 07 2018 at 01:27):

@Simon Hudon very nice, sir.


Last updated: May 10 2021 at 19:16 UTC