Zulip Chat Archive

Stream: general

Topic: refine_struct cases


view this post on Zulip Yury G. Kudryashov (Apr 08 2020 at 04:31):

I called refine_struct { .. } on an equiv goal, and it generated 4 goals, first of them labeled case equiv, to_fun.

view this post on Zulip Yury G. Kudryashov (Apr 08 2020 at 04:31):

How do I focus those goals by name?

view this post on Zulip Yury G. Kudryashov (Apr 08 2020 at 04:32):

I tried case equiv to_fun, case equiv.to_fun, case "equiv, to_fun"

view this post on Zulip Johan Commelin (Apr 08 2020 at 04:35):

@Simon Hudon :up:

view this post on Zulip Mario Carneiro (Apr 08 2020 at 05:58):

You can't, at least not with case

view this post on Zulip Mario Carneiro (Apr 08 2020 at 05:59):

case is explicitly filtering for cases that are tagged with _case or _case_simple, while refine_struct generates cases tagged with _field

view this post on Zulip Mario Carneiro (Apr 08 2020 at 06:02):

I hadn't realized that there is an additional hidden tag marker like this. This seems like a dubious feature, since there is no UI indication that this case is any different from the kind of case you get from the inductive tactic

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 07:31):

Ooh tag markers. That's new

view this post on Zulip Simon Hudon (Apr 08 2020 at 14:48):

with refine_struct, you use field instead of case. You use it as field my_struct_field { tactic }

view this post on Zulip Simon Hudon (Apr 08 2020 at 14:52):

You can use have_field to stand for have field := @my_struct.some_field


Last updated: May 14 2021 at 22:15 UTC