The Coq mailing list

["" <judy AT mail.ccnu.edu.cn>]

HI:

here some question:
1:

Section A1.
Vaiable U:Type.
Definition Ensemble: U->Prop.
End A1.
Section A2.
Variable U:Type.
Definition Sets:= Ensemble U.
.
.
End A2

Above is a way to rename Ensemble with Sets.

Why here is not OK:

Section A3.
Vaiable U:Type.
Definition Ensemble: U->Prop.
Definition Sets:= Ensemble U.

,,
End A3.

and if I define Sets directly this way:

Section A4.
Vaiable U:Type.
Definition Sets: U->Prop.

Does Sets here is different from the "Sets" in Section A1,and A2 in the first
way.

2:
if I want to define a set(not the keyword in coq) A={a,b,c},only has 4 
elements. 
Inductive A:Set:=|a:A|b:A|c:A.
in this way ,Does here A means {a,b,c,},,or means sets composed by some of the
elment in {a,b,c},which means anyone of 
{a}{b}{c}{a,b}{a,c}{b,c}{a,b,c}and{null}?
 
Variable a b c:U.
Inductive A:Ensemble:=|a1:In A a |a2:In A b|a3:In A c.
Does this way OK?

So my question is how to define a definite set (not the keyword in coq)

In question 1 ,

Section A1.
Vaiable U:Type.
Definition Ensemble: U->Prop.
End A1.
Section A2.
Variable U:Type.
Definition Sets:= Ensemble U.

Inductive A:Set:=|a:A|b:A|c:A.

Definition Aset:=Sets A.

here Aset meas {a,b,c},,or meas anyone of
{a}{b}{c}{a,b}{a,c}{b,c}{a,b,c}and{null}?


looking forward your help?

yours sincerely 

Judy.