Zulip Chat Archive

Stream: general

Topic: instances


view this post on Zulip Jakob von Raumer (Oct 20 2018 at 10:15):

Can someone explain this?

failed to synthesize type class instance for
TL : Type u,
[...]
_inst_9 : is_contr TL,
[...]
 is_contr TL

Even if I set pp.all true, it shows that TL is the right thing and there's no hidden difference...

view this post on Zulip Kevin Buzzard (Oct 20 2018 at 10:55):

Did you try using letI to add the instance to the type class inference system? I appreciate that its name indicates that it should be in it already..

view this post on Zulip Jakob von Raumer (Oct 20 2018 at 10:58):

The environment looks like this:

@[hott] def pushout_of_embedding {n : ₋₂} [is_embedding g] :
  Π [is_trunc n TL] [is_trunc n TR] [is_trunc n BL],
  is_trunc n (pushout f g) :=
begin
  induction n with n IH,
  { intros, apply base_case,  }
end

So it's mentioned after the :, maybe that's what prevents it from being a local instance?

view this post on Zulip Kevin Buzzard (Oct 20 2018 at 11:08):

Yes that's exactly it.

view this post on Zulip Kevin Buzzard (Oct 20 2018 at 11:08):

You need to explicitly add it to the instance list with letI

view this post on Zulip Jakob von Raumer (Oct 20 2018 at 11:08):

Okay, thanks :+1:

view this post on Zulip Kevin Buzzard (Oct 20 2018 at 11:10):

Leo changed this behaviour a few months ago. Nothing right of the colon goes in any more

view this post on Zulip Kenny Lau (Oct 20 2018 at 12:44):

you should use resetI there instead of letI


Last updated: May 17 2021 at 22:15 UTC