instances

Stream: general

[Jakob von Raumer]

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...

[Kevin Buzzard]

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..

[Jakob von Raumer]

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?

[Kevin Buzzard]

Yes that's exactly it.

[Kevin Buzzard]

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

[Jakob von Raumer]

Okay, thanks :+1:

[Kevin Buzzard]

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

[Kenny Lau]

you should use resetI there instead of letI