zohaze (Dec 16 2022 at 17:46): 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'?
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.
zohaze (Feb 09 2023 at 15:10):It works,thank u.
Last updated: Oct 08 2024 at 14:01 UTC