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'?
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.
It works,thank u.
Last updated: Oct 04 2023 at 22:01 UTC