pianke (Jan 22 2023 at 08:11): pianke (Jan 22 2023 at 08:11):I am defining the following function (in Coq) and have problem in storing the result in output list.
Some one like to help me
1) I have list nat l1=[ x1,x2,x3...x-1,xn]
I am passing x1 to a function f (f x1) and function generate a list nat l2 =[y1,y2,..ym]
In case of existence of x2 in l2 , want to store result in a output list which shows that yn of l2
matches with x2
2) Then repeat this for all elements of l1 like (f x2) checking existence of x3 in sequence...
and store result in same output list.
3) In case of mismatch stop the process and show list upto that point only.
Regards.
Last updated: Apr 20 2024 at 14:01 UTC