The Coq mailing list

["Patricia Peratto" <psperatto AT adinet.com.uy>]

I want to define an inductive set without using forall

(using only parameters in the type definition and in the

constructor).

 

My definition is below:

 

Inductive W (A1:Set)(A2:A1->Set):Type:=
| sup (b:A1)
        (u:(x:A2 b)W A1 A2)
                : W A1 A2.

 

I get the error message:

 

Error: The reference x was not found in the current

environment.

 

Someone knows how to define it?

Regards

Patricia