Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] parameters

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] parameters


Chronological Thread 
  • 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



Archive powered by MHonArc 2.6.18.

Top of Page