(* If you are working with lists, some syntactic sugar may be useful.
   Try the following.
   Open Local Scope list_scope.
   opens the nice notation, using :: ++ etc. You can also "match" on 
   x :: l when defining a Fixpoint. *)

Require Import List.

Open Scope list_scope.

Check 1 :: 2 :: nil.

Definition l := 1::2::nil.
Definition k := 2::3::5::nil.

Eval compute in k ++ l.