Zulip Chat Archive
Stream: triage
Topic: issue #7691: to_additive-like attribute for order_dual
Random Issue Bot (Dec 10 2021 at 14:20):
Today I chose issue 7691 for discussion!
to_additive-like attribute for order_dual
Created by @Bryan Gin-ge Chen (@bryangingechen) on 2021-05-22
Labels: meta, feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Bryan Gin-ge Chen (Dec 10 2021 at 14:41):
I doubt this is worth working on in Lean 3, but maybe should be considered as a feature-request for the Lean 4 version of to_additive.
Random Issue Bot (Apr 04 2022 at 14:14):
Today I chose issue 7691 for discussion!
to_additive-like attribute for order_dual
Created by @Bryan Gin-ge Chen (@bryangingechen) on 2021-05-22
Labels: meta, feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Jun 10 2022 at 14:19):
Today I chose issue 7691 for discussion!
to_additive-like attribute for order_dual
Created by @Bryan Gin-ge Chen (@bryangingechen) on 2021-05-22
Labels: meta, feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Jun 22 2022 at 14:20):
Today I chose issue 7691 for discussion!
to_additive-like attribute for order_dual
Created by @Bryan Gin-ge Chen (@bryangingechen) on 2021-05-22
Labels: meta, feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Aug 01 2022 at 14:16):
Today I chose issue 7691 for discussion!
to_additive-like attribute for order_dual
Created by @Bryan Gin-ge Chen (@bryangingechen) on 2021-05-22
Labels: t-meta, feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Sep 27 2022 at 14:34):
Today I chose issue 7691 for discussion!
to_additive-like attribute for order_dual
Created by @Bryan Gin-ge Chen (@bryangingechen) on 2021-05-22
Labels: t-meta, feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Nov 08 2022 at 14:10):
Today I chose issue 7691 for discussion!
to_additive-like attribute for order_dual
Created by @Bryan Gin-ge Chen (@bryangingechen) on 2021-05-22
Labels: t-meta, feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Jun 15 2023 at 14:07):
Today I chose issue 7691 for discussion!
to_additive-like attribute for order_dual
Created by @Bryan Gin-ge Chen (@bryangingechen) on 2021-05-22
Labels: t-meta, feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Last updated: Dec 20 2023 at 11:08 UTC