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: Feb 08 2023 at 23:03 UTC