inheritance of type class instances

Stream: new members

[Thomas Kantholz]

hi,
i have been working on some basics of first order logic.
i would like to define a clause as a multiset of literals but encountered a problem since the type class instances of multisets are not inherited by the new type.

constant σ : signature
constant l₁ : σ.literal

def signature.clause (σ : signature) := multiset σ.literal

--failed to synthesize type class instance for...
--noncomputable def c₁ : σ.clause := {l₁}

--i could make this work by explicitly specifying the type however this is very tedious
noncomputable def c₂ : σ.clause := ({l₁} : multiset σ.literal)

is there some way to inherit the type class instances of a type?

[Eric Wieser]

Putting @[reducible] before the first def would do the job

[Anne Baanen]

An alternative is to use the derive annotation, for example @[derive has_singleton] should fix that specific issue.

[Thomas Kantholz]

thanks!