coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] parameters

From: Stéphane Glondu <steph AT glondu.net>
To: Patricia Peratto <psperatto AT adinet.com.uy>
Cc: coqclub <coq-club AT inria.fr>
Subject: Re: [Coq-Club] parameters
Date: Thu, 14 Jun 2012 21:22:10 +0200
Openpgp: id=49881AD3

Le 14/06/2012 18:39, Patricia Peratto a écrit :
> Inductive W (A1:Set)(A2:A1->Set):Type:=
> | sup (b:A1)
> (u:(x:A2 b)W A1 A2)
> : W A1 A2.

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

Note that it is not always possible to not use forall.

Cheers,

--
Stéphane

[Coq-Club] parameters, Patricia Peratto, 06/14/2012
- Message not available
  - Re: [Coq-Club] parameters, Patricia Peratto, 06/14/2012
- 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