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
cbn for example) in all assumptions without having to list them all via
unfold <foo> in h_1 h_2 ... h_n?
unfold foo at 1 and
unfold foo/simpl/cbn in * exist.
But this notation refers to a definition, right?
Paolo Giarrusso said:
unfold foo at 1and
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.
Tobias Schmude has marked this topic as resolved.
Last updated: Jan 28 2023 at 06:30 UTC