Zulip Chat Archive

Stream: general

Topic: a tactic for copying lemmas when using old_structure_cmd


view this post on Zulip Scott Morrison (Apr 14 2021 at 10:22):

Do we have some automation available for copying lemmas from X to Y, when Y extends X with old_structure_cmd.

view this post on Zulip Scott Morrison (Apr 14 2021 at 10:23):

I'd like to be able to list (or even collect automatically?) lemmas about X, and have corresponding lemmas about Y be built for me.

view this post on Zulip Scott Morrison (Apr 14 2021 at 10:25):

At the moment, e.g. with monoidal_functor, we have lots of annoying F.to_functor.map_comp. map_comp isn't a structure field of functor, it's a lemma in terms of the actual field map_comp', so I don't automatically get a version of it for monoidal_functor.

view this post on Zulip Mario Carneiro (Apr 14 2021 at 10:34):

It seems like a better solution here would be to register that dot notation should look in the functor namespace for lemmas if monoidal_functor doesn't have it

view this post on Zulip Mario Carneiro (Apr 14 2021 at 10:35):

Does the lemma apply if you write functor.map_comp F?

view this post on Zulip Eric Wieser (Apr 14 2021 at 10:56):

Doesn't it need to do functor.map_comp F.to_functor?

view this post on Zulip Eric Wieser (Apr 14 2021 at 10:57):

But then that statement is about F.to_functor not F, so while defeq won't work for rewrites

view this post on Zulip Scott Morrison (Apr 14 2021 at 11:39):

No, it doesn't work with just functor.map_comp F.


Last updated: May 13 2021 at 17:42 UTC