Stream: Coq users

Topic: ✔ Scope of unfold: specific instances and complete context


view this post on Zulip Tobias Schmude (May 05 2022 at 06:39):

Is it possible to unfold only a specific instance (of a notation in my case) in some expression?
In what I'm trying to do there is a binary infix notation ;; which can denote two (related but distinct) things (FYI: composition of morphisms in a category/displayed category) and also hides crucial data (the (displayed) category they're living in as well as the (co)domain objects of the morphisms). This can lead to ambiguities, so it can help to unfold it. As this notation may appear multiple times in an expression, sometimes I want to unfold only a specific instance, but not the others. Is there some refinement of unfold ";;" (in <foo>) that allows me to specify which occurrence of ";;" to unfold?

Going into the other direction: is there a way to unfold <foo> (or simpl/cbn for example) in all assumptions without having to list them all via unfold <foo> in h_1 h_2 ... h_n?

view this post on Zulip Paolo Giarrusso (May 05 2022 at 06:52):

unfold foo at 1 and unfold foo/simpl/cbn in * exist.

view this post on Zulip Paolo Giarrusso (May 05 2022 at 06:53):

But this notation refers to a definition, right?

view this post on Zulip Tobias Schmude (May 06 2022 at 10:01):

Paolo Giarrusso said:

unfold foo at 1 and unfold foo/simpl/cbn in * exist.

Thanks! This has made me aware of occurrence clauses. It's still annoying to guess occurrence numbers since most of the occurrences are hidden by the notation though. I think I should play around with the Printing Notation flag.

view this post on Zulip Notification Bot (May 07 2022 at 10:43):

Tobias Schmude has marked this topic as resolved.


Last updated: Jan 28 2023 at 06:30 UTC