coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jean-Francois Monin <jean-francois.monin AT imag.fr>
- To: Patricia Peratto <psperatto AT adinet.com.uy>
- Cc: coqclub <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] parameters
- Date: Fri, 15 Jun 2012 06:52:07 +0800
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
- [Coq-Club] parameters, Patricia Peratto, 06/14/2012
- Message not available
- Re: [Coq-Club] parameters, Patricia Peratto, 06/14/2012
- Message not available
- Re: [Coq-Club] parameters, Adam Chlipala, 06/14/2012
- Re: [Coq-Club] parameters, Stéphane Glondu, 06/14/2012
- Re: [Coq-Club] parameters, Jean-Francois Monin, 06/15/2012
Archive powered by MHonArc 2.6.18.