The Coq mailing list

["Patricia Peratto" <psperatto AT adinet.com.uy>]

Hello, I have defined the list inductive set in the following way:

 

Inductive List :forall(A:Type),Type :=
|nil : forall(A:Type),List A
|cons :forall(A:Type)(a:A)(l:(List A)),List A.

 

The corresponding recursive operator is

 

List_rect : forall P: forall A:Type, List A -> Type,
            (forall A:Type, P A (nil A)) ->
            (forall (A:Type) (a:A)(l:List A), P A l -> P A (cons A a l)) ->
            forall (A:Type)(l:List A), P A l

 

I want to define the function map using List_rect and with
the type that I show below:

 

Definition map : forall (A B:Type)(F:A->B)
(l:List A), List B :- ............

 

I have tried different ways but I couldn´t define it.

 

Can someone help me with this definition?

 

Regards,
Patricia Peratto