Stream: Coq users

Topic: arrange elements


view this post on Zulip zohaze (Mar 14 2023 at 18:10):

I have two natural number lists l1 & l2. I am finding match element of l1 in l2 , in case it is found then remove it from l2 and add it infront of l2 else empty list.
l1=[2,3,4] l2=[5,3,6,2,8,4]
reult: 4,3,2,5,6,8

Fixpoint find  (l1 l2: list nat ) : list nat :=
  match  l1,l2  with
  | nil , nil => nil
  | [], a2::t =>  []
  | a1::t , [] =>  []
  | a1::t1,a2::t2=> if ( eq a1 a2) then  (remove a1 t2)  a1 ::t2 find t1 t2 else []

Last updated: Oct 04 2023 at 20:01 UTC