Zulip Chat Archive

Stream: general

Topic: Cannot find instance

view this post on Zulip AHan (Dec 04 2018 at 06:16):

In mathlib/data/finsupp.lean the instance has_add of finsupp structure was already proved,
but in t he following example, it failed to synthesize type class instance for has_add...
Don't understand what instance I missed...

import data.finsupp
variables {α : Type*} {β : Type*} [has_zero α] [has_zero β] [add_monoid α] [add_monoid β]
variables [decidable_eq α] [decidable_eq β]

lemma support_contain_a' (a b : α  β) : a.support  (a + b).support := sorry

Last updated: May 15 2021 at 22:14 UTC