The Coq mailing list

[silviu andrica <silviu_andrica AT yahoo.com>]

Hello,
  Today is my first day of Coq and I want to write a function in Coq that checks if a list is a sublist of another list. I was thinking somewhat around the lines of

Definition sublist ( big_list sub_list : list ) := (exists a : list, b : list) -> a++sub_list++b = big_list .

And afterwards have this exported to OCaml.

But I cannot do, can some one help?

Best regards,
  Silviu