James Wood (Aug 16 2022 at 12:54): James Wood (Aug 16 2022 at 12:54):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]..
Paolo Giarrusso (Aug 16 2022 at 13:33):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?)
Paolo Giarrusso (Aug 16 2022 at 13:33):your example should work as destruct a as [ [x|y]%f | z ].
Paolo Giarrusso (Aug 16 2022 at 13:34):(ssreflect has its own syntax, but you don't need it just for this)
James Wood (Aug 16 2022 at 13:49):Aha, nice, I'll give it a go!
Notification Bot (Aug 16 2022 at 13:51):James Wood has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC