Zulip Chat Archive
Stream: general
Topic: autogenerate copy
Johan Commelin (Mar 10 2022 at 14:59):
src#add_monoid_hom.copy is written by hand, and so are many other copys. How hard would it be to write an attribute @[copy] that we can slap on defs and structures in order to auto-generate their copy constructor?
Eric Wieser (Mar 10 2022 at 15:11):
What would it mean on defs?
Johan Commelin (Mar 10 2022 at 15:17):
Aah, I guess that doesn't make sense. So let's just focus on structure (and class).
Yaël Dillies (Mar 10 2022 at 15:23):
Had this on my mind too!
Yaël Dillies (Mar 10 2022 at 15:23):
The problem is with some structures which use copy to mean something else. Ex: docs#finpartition.copy. Culprit: me.
Johan Commelin (Mar 10 2022 at 15:24):
I guess that should be congr instead of copy?
Yaël Dillies (Mar 10 2022 at 15:29):
Oh yeah maybe.
Yaël Dillies (Mar 10 2022 at 15:29):
Could this one be autogenerated as well?
Eric Wieser (Mar 10 2022 at 15:32):
I guess fin.cast is analogous to finpartition.copy?
Eric Wieser (Mar 10 2022 at 15:32):
Can we think of other similar examples of things which are just definitionally nicer versions of cast h?
Bhavik Mehta (Mar 10 2022 at 16:23):
Eric Wieser (Mar 10 2022 at 16:32):
That's not a definitionally nicer version though, that's just a bundled cast
Eric Wieser (Mar 10 2022 at 16:33):
I'm talking about things where foo h x = cast h x propositionally but not definitionally, like fin.cast and finpartition.cast
Bhavik Mehta (Mar 10 2022 at 17:42):
Ah I see!
Last updated: Dec 20 2023 at 11:08 UTC