auto deriving instances

Stream: general

[Zesen Qian]

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

[Kenny Lau]

don't use them :)

[Zesen Qian]

I feel type synonym is useful in development.

[Kenny Lau]

pretty sure you can't find it anywhere in mathlib

[Simon Hudon]

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

[Simon Hudon]

Otherwise, you can do

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

[Zesen Qian]

@Simon Hudon very nice, sir.