The Coq mailing list

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

Not, I want to define the constructor without
using forall.

----- Original Message ----- 
From: "Thomas Braibant" <thomas.braibant AT gmail.com>
To: "Patricia Peratto" 
<psperatto AT adinet.com.uy>
Sent: Thursday, June 14, 2012 1:44 PM
Subject: Re: [Coq-Club] parameters


Is this what you wanted to achieve?

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


Thomas


On Thu, Jun 14, 2012 at 12:39 PM, Patricia Peratto
<psperatto AT adinet.com.uy>
 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