The Coq mailing list

[Christine Paulin <Christine.Paulin AT lri.fr>]

The basic idea for inductive definitions is that it should be in a
sort s (Set in your case) if each type of each argument of each
constructor is in the same sort s.
In your case the constructor cons1 expect an argument (A) of type Set.
We have Set is of sort Type so the all definition should be in sort 
Type.

There is an exception for the sort Prop (but eliminations on inductive
def of sort Prop are restricted)
The older versions of Coq allows Set to be impredicative (so your
definition would type-check with a restricted notion of elimination)
this behavior can be also obtained on the current version 
with the coqtop -impredicative-set
option

Christine Paulin

Carpentier Helene writes:
 > Hi,
 > I'm a new Coq user 
 > I tried to define and inductive type 
 >  ind_type:
 > Inductive ind_type:Set:=
 > cons1:forall (A:Set), A->ind_type.
 > 
 > I got the following error:
 > User error: Large non-propositional inductive types
 > must be in Type
 > 
 > why is this the case? 
 > I checked the type of the term (forall (A:Set), A) and
 > found Type, is this the cause?
 > 
 > Thanks
 > Helene
 > 
 > 
 > 
 >      
 > 
 >      
 >              
 > Découvrez le nouveau Yahoo! Mail : 250 Mo d'espace de stockage pour vos 
 > mails ! 
 > Créez votre Yahoo! Mail sur http://fr.mail.yahoo.com/
 > --------------------------------------------------------
 > Bug reports: http://coq.inria.fr/bin/coq-bugs
 > Archives: http://pauillac.inria.fr/pipermail/coq-club
 >           http://pauillac.inria.fr/bin/wilma/coq-club
 > Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

-- 
  Christine Paulin-Mohring             mailto : 
Christine.Paulin AT lri.fr
  LRI, UMR 8623 CNRS, Bat 490, Université Paris Sud,   91405 ORSAY Cedex 
  tel : (+33) (0)1 69 15 66 35         fax : (+33) (0)1 69 15 65 86