The Coq mailing list

[Marko Malikovi� <marko AT ffri.hr>]

Greetings,

I need to work with small subset of natural numbers, from 1 to 5.
Normally, I can define it in this way:

Inductive in_subset : nat -> Prop := in_subset_def : forall x : nat,
1<=x<=5 -> in_subset x.

But, for my needs is more appropriate to have definition like this:

Inductive in_subset : nat -> Prop :=
| C1 : in_subset 1
| C2 : in_subset 2
| C3 : in_subset 3
| C4 : in_subset 4
| C5 : in_subset 5.

Is something theoretically (from view of Cic) wrong with this kind of
definitions?

Thank you very much and greetings,

Marko Malikoviæ