The Coq mailing list

[Julien Tesson <julien.tesson AT univ-orleans.fr>]

(*
Hi,
I have found a behavior in Coq that I don't understand :
If i define a type A in Prop like
*)

Definition A:= 1=1.

(*
 and then typecheck the type (list A),
*)

Check (list A).

(*
then coq reply
list A
    : Set
Why is it in Set and not in Prop ? or at least in Type, as list as type Type 
-> Type ?

Furthermore I was thinking that it was not possible to build values in Set 
using values in Prop
but the following definition does :
*)

Definition f := fun x : A => x::nil.

(*
Can someone explain me why does Coq behave like this ?


-- 
Julien Tesson

Doctorant - ATER
Laboratoire d'Informatique Fondamentale d'Orléans
Département Informatique
Université d'Orléans

Tel : 02 38 49 25 81
Fax : 09 56 45 86 27
http://tesson.julien.free.fr/




*)