Paolo Giarrusso (Aug 16 2022 at 13:33): 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: Feb 08 2023 at 23:03 UTC