Stream: Coq users

Topic: ✔ View patterns


view this post on Zulip 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?)

view this post on Zulip Paolo Giarrusso (Aug 16 2022 at 13:33):

your example should work as destruct a as [ [x|y]%f | z ].

view this post on Zulip Paolo Giarrusso (Aug 16 2022 at 13:34):

(ssreflect has its own syntax, but you don't need it just for this)

view this post on Zulip James Wood (Aug 16 2022 at 13:49):

Aha, nice, I'll give it a go!

view this post on Zulip 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