Zulip Chat Archive

Stream: new members

Topic: Coercion local homeomorph

view this post on Zulip Nicolò Cavalleri (Aug 29 2020 at 14:17):

Is it a bad idea to define a coercion from from homeomorph to local_homeomorph so that one does not have to write .to_local_homeomorph each time?

view this post on Zulip Reid Barton (Aug 29 2020 at 14:29):

Based on https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/preferred.20alternatives.20to.20type.20ascriptions.20everywhere.3F/near/208213580, I don't think it would help as much as one would hope

Last updated: May 13 2021 at 21:12 UTC