Zulip Chat Archive

Stream: triage

Topic: issue #946: data.nat.cast.cast is too general to be an in...


view this post on Zulip Random Issue Bot (Nov 26 2020 at 14:20):

Today I chose issue 946 for discussion!

data.nat.cast.cast is too general to be an instance
Created by @None (@simonjwinwood) on 2019-04-17
Labels:

Is this issue still relevant? Any recent updates? Anyone making progress?

view this post on Zulip Kevin Buzzard (Nov 26 2020 at 15:26):

Related: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Friday.20afternoon.20puzzle.20--.2037.20.E2.88.88.2037.3F/near/217418582

view this post on Zulip Random Issue Bot (Dec 16 2020 at 14:25):

Today I chose issue 946 for discussion!

data.nat.cast.cast is too general to be an instance
Created by @None (@simonjwinwood) on 2019-04-17
Labels:

Is this issue still relevant? Any recent updates? Anyone making progress?

view this post on Zulip Eric Wieser (Dec 16 2020 at 14:30):

docs#nat.cast

view this post on Zulip Random Issue Bot (Feb 20 2021 at 14:19):

Today I chose issue 946 for discussion!

data.nat.cast.cast is too general to be an instance
Created by @None (@simonjwinwood) on 2019-04-17
Labels:

Is this issue still relevant? Any recent updates? Anyone making progress?

view this post on Zulip Random Issue Bot (Mar 05 2021 at 14:20):

Today I chose issue 946 for discussion!

data.nat.cast.cast is too general to be an instance
Created by @None (@simonjwinwood) on 2019-04-17
Labels:

Is this issue still relevant? Any recent updates? Anyone making progress?

view this post on Zulip Random Issue Bot (Mar 13 2021 at 14:21):

Today I chose issue 946 for discussion!

data.nat.cast.cast is too general to be an instance
Created by @None (@simonjwinwood) on 2019-04-17
Labels:

Is this issue still relevant? Any recent updates? Anyone making progress?

view this post on Zulip Scott Morrison (Mar 13 2021 at 22:57):

It seems at the conclusion of #5664, which added nat.bin_cast, there was a suggestion to try making it the implementation of the coercion. Did anyone attempt this?

view this post on Zulip Scott Morrison (Mar 13 2021 at 22:58):

It seems that it would be a satisfactory resolution to this old issue!

view this post on Zulip Yakov Pechersky (Mar 14 2021 at 00:23):

Yes, I tried doing it. But too many things use nat.cast in places where there is no proof of associativity, commutativity, or '0+0=0' which is what makes nat.cast and nat.bin_cast probably equal

view this post on Zulip Yakov Pechersky (Mar 14 2021 at 00:24):

For example, it was a slog to try to get it working for pgame.short, so I abandoned the attempt.

view this post on Zulip Scott Morrison (Mar 14 2021 at 00:40):

Ah, thanks! It's nice to know the combinatorial games are a good test case for this issue.

view this post on Zulip Scott Morrison (Mar 14 2021 at 00:41):

Could we try something like "use nat.bin_cast by default, but it's okay, e.g. in pgame, to instead use the more primitive coercion"?

view this post on Zulip Yakov Pechersky (Mar 14 2021 at 00:56):

So, instance priority based add_comm_monoid -> nat.bin_cast, and nat.cast as lower priority?

view this post on Zulip Scott Morrison (Mar 14 2021 at 01:14):

Yes.

view this post on Zulip Scott Morrison (Mar 14 2021 at 01:14):

Maybe it ends up being confusing.


Last updated: May 09 2021 at 16:20 UTC