Zulip Chat Archive

Stream: new members

Topic: inheritance of type class instances

Thomas Kantholz (Jan 04 2023 at 19:08):

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 (Jan 04 2023 at 19:34):

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

Anne Baanen (Jan 05 2023 at 10:21):

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

Thomas Kantholz (Jan 05 2023 at 14:45):


Last updated: Dec 20 2023 at 11:08 UTC