Zulip Chat Archive
Stream: general
Topic: Why doesn't unfold propagate tags?
Kenny Lau (Apr 11 2020 at 17:06):
Why doesn't unfold propagate tags?
Kenny Lau (Apr 13 2020 at 09:48):
@Mario Carneiro
Mario Carneiro (Apr 13 2020 at 09:48):
what kind of question is this?
Mario Carneiro (Apr 13 2020 at 09:48):
it doesn't because no one made it do so
Mario Carneiro (Apr 13 2020 at 09:48):
PR
Johan Commelin (Apr 13 2020 at 09:49):
I think tags are not really supported in our ecosystem
Johan Commelin (Apr 13 2020 at 09:50):
Sometimes they are there... and that's about it
Chris Hughes (Apr 15 2020 at 00:24):
What does propogate tags mean?
Scott Morrison (Apr 15 2020 at 01:41):
After you run cases, the new goals produced will be labelled something like case nil and case cons at the top. The propagate_tags tactic runs another tactic, and copies those tags over to the new goals.
Scott Morrison (Apr 15 2020 at 01:42):
The tags are hacky add-on, and most of the core tactics will discard them, so this is a little wrapper to "carry the tags around the side".
Last updated: Dec 20 2023 at 11:08 UTC