Zulip Chat Archive

Stream: general

Topic: fun_setoid

view this post on Zulip Reid Barton (May 11 2019 at 00:22):

Some change to mathlib in the last month or so (I don't know which) caused lean-homotopy-theory to break because Lean now wants to synthesize a setoid instance on the hom types of Top using subtype.setoid and fun_setoid from core, while I want to use a different one. I don't really understand how this is possible; for now I'm working around it by setting an instance priority. But, I am pretty sure that fun_setoid (in init/funext.lean) should not be a global instance, just an instance for the scope of the proof of funext. Maybe that can be changed in 3.5.0?

Last updated: May 09 2021 at 20:11 UTC