Get decidable_eq from classical

Stream: new members

[Marcus Rossel]

What is the right incantation for automatically getting decidable_eq instances as type class arguments?
For example, if we have:

import data.finset

inductive t1
inductive t2

def t1_to_t2 : t1 → t2 := sorry

def t_image (f : finset t1) : finset t2 :=
  f.image t1_to_t2

The last line has the error:

failed to synthesize type class instance for
f : finset t1
⊢ decidable_eq t2

The only way I know how to fix this, using classical, is:

noncomputable def t_image (f : finset t1) : finset t2 :=
  @finset.image _ _ (classical.dec_eq _) t1_to_t2 f

Is there a simpler way, where I don't have to provide the type class instance explicitly?

Thanks :)

[Scott Morrison]

open_locale classical