Zulip Chat Archive
Stream: triage
Topic: issue #3837: `@[simps]` does not consider projections of ...
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?
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?
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?
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: Dec 20 2023 at 11:08 UTC