Zulip Chat Archive

Stream: general

Topic: algebra_map over nat.cast

Yaël Dillies (Oct 15 2022 at 14:55):

I don't have a MWE, but it should be easy to reproduce by having big enough imports (topology.metric_space.isometry I suspect?). The coercion from ℕ → ℝ now goes through docs#algebra_map.has_lift_t since @Kevin Buzzard's PR. I think they are defeq, but we should certainly monitor the situation and maybe tweak the priorities so that nat.cast stays over.

Yaël Dillies (Oct 15 2022 at 15:00):

I'm mostly worried about positivity extensions, like docs#tactic.positivity_coe breaking. @Anne Baanen, is your "unification workaround" able to fix the potential breakage?

Kevin Buzzard (Oct 15 2022 at 22:05):

OMG did that get merged? I've been quite busy this month...

Eric Wieser (Oct 15 2022 at 23:42):

Unification sounds like the right solution in the first place, not a workaround

Eric Wieser (Oct 15 2022 at 23:42):

Tactics should never syntactically match on instances

Last updated: Dec 20 2023 at 11:08 UTC