Is there any tactic comparable to
destruct that would let me write something like view patterns within intropatterns? For example, it would be nice to write
destruct a as [ f -> [x|y] | z ]. and it produce the same subgoals (but arranged linearly) as
destruct a as [xy|z]. destruct (f xy) as [x|y]..
ah, you mean GHC view patterns, not ssreflect views — you can then use
intro_pattern%f (I mostly use it for lemmas, but I _think_ it should work for functions as well?)
your example should work as
destruct a as [ [x|y]%f | z ].
(ssreflect has its own syntax, but you don't need it just for this)
Aha, nice, I'll give it a go!
James Wood has marked this topic as resolved.
Last updated: Sep 23 2023 at 07:01 UTC