The Coq mailing list

[Carpentier Helene <helene_carpentier2000 AT yahoo.fr>]

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/