Tobias Schmude (May 05 2022 at 06:39): 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?
Paolo Giarrusso (May 05 2022 at 06:52):unfold foo at 1 and unfold foo/simpl/cbn in * exist.
Paolo Giarrusso (May 05 2022 at 06:53):But this notation refers to a definition, right?
Tobias Schmude (May 06 2022 at 10:01):Paolo Giarrusso said:
unfold foo at 1andunfold 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.
Notification Bot (May 07 2022 at 10:43):Tobias Schmude has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC