Zulip Chat Archive

Stream: triage

Topic: issue #3837: `@[simps]` does not consider projections of ...


view this post on Zulip Random Issue Bot (Nov 09 2020 at 14:18):

Today I chose issue 3837 for discussion!

@[simps] does not consider projections of ancestors as legitimate definitions for has_coe_to_fun
Created by @Simon Hudon (@cipher1024) on 2020-08-17
Labels: maybe-later, meta

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

view this post on Zulip Random Issue Bot (Dec 09 2020 at 14:24):

Today I chose issue 3837 for discussion!

@[simps] does not consider projections of ancestors as legitimate definitions for has_coe_to_fun
Created by @Simon Hudon (@cipher1024) on 2020-08-17
Labels: maybe-later, meta

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

view this post on Zulip Random Issue Bot (Jan 17 2021 at 14:43):

Today I chose issue 3837 for discussion!

@[simps] does not consider projections of ancestors as legitimate definitions for has_coe_to_fun
Created by @Simon Hudon (@cipher1024) on 2020-08-17
Labels: maybe-later, meta

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

view this post on Zulip Random Issue Bot (Apr 08 2021 at 14:24):

Today I chose issue 3837 for discussion!

@[simps] does not consider projections of ancestors as legitimate definitions for has_coe_to_fun
Created by @Simon Hudon (@cipher1024) on 2020-08-17
Labels: maybe-later, meta

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


Last updated: May 18 2021 at 22:15 UTC