Stream: Coq users

Topic: destruct command

view this post on Zulip zohaze (Dec 16 2022 at 17:46):

I have a element D of some datatype.Its notation is D'(x1 x2 y1 y2) . While x & y are nat values.
I want to match D' with another element of same type B(x3 x4 _ _). Don't want to consider y1 & y2 during matching.
Only problem is that when i destruct D' as [ x1 x2 _ _].it gives error.
How i should destruct D'?

view this post on Zulip Michael Soegtrop (Dec 16 2022 at 18:32):

If I understand you right D' is a constructor for type D taking for arguments. You have to supply all arguments to the constructor in order to be able to destruct it. So you can say destruct (D'(x1 x2 y1 y2)). If this doesn't work for you, please give more details - preferably a small piece of code which compiles as is.

view this post on Zulip zohaze (Feb 09 2023 at 15:10):

It works,thank u.

Last updated: May 25 2024 at 19:02 UTC