The Coq mailing list

[Jean-Francois Monin <jean-francois.monin AT imag.fr>]

Do you mean:
Inductive W (A1:Set) (A2:A1->Set) : Type := 
  | sup (b: A1) (u: (forall x: A2 b, W A1 A2)) : W A1 A2.

?

Regards,
Jean-Francois

On Thu, Jun 14, 2012 at 01:39:16PM -0300, Patricia Peratto wrote:
>    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