The Coq mailing list

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

> Assume I define:
>
> Inductive Eq : forall (A:Type)(x:A),A->Type :=
> |refleq : forall (A:Type)(x:A),Eq A x x.
>
> I can instead define Eq with parameters and arrow as follows
>
> Inductive Eq (A:Type)(x:A):A->Type:=
> |refleq: Eq A x x.
>
> The question is if I can avoid to use forall and use instead parameters 
> and arrow.
>
>
> ----- Original Message ----- 
> From: "Adam Chlipala" <adamc AT csail.mit.edu>
> To: "Patricia Peratto" 
> <psperatto AT adinet.com.uy>
> Cc: "coqclub" 
> <coq-club AT inria.fr>
> Sent: Saturday, April 21, 2012 4:19 PM
> Subject: Re: [Coq-Club] parameter
>
>
> > Patricia Peratto wrote:
> > > In case of a formation rule, can I replace in an inductive declaration 
> > > of a type a forall
> > > by parameters and arrow?
> >
> > I'm afraid I don't understand again.  Another example, please?
> >
> > > ----- Original Message ----- From: "Adam Chlipala" 
> > > <adamc AT csail.mit.edu>
> > > To: "Patricia Peratto" 
> > > <psperatto AT adinet.com.uy>
> > > Cc: "coqclub" 
> > > <coq-club AT inria.fr>
> > > Sent: Saturday, April 21, 2012 3:45 PM
> > > Subject: Re: [Coq-Club] parameter
> > >
> > >
> > > > Patricia Peratto wrote:
> > > > > Yes, my question is other.
> > > > > What I mean is if always that I have an explicit forall
> > > > > in a definition I can replace it by parameters and  arrow. By example
> > > > > I can write:
> > > > >
> > > > > cons (a:A)(l:List A):List A
> > > > >
> > > > > or
> > > > >
> > > > > cons : A->List A->List A
> > > > >
> > > > > instead of
> > > > > cons : forall(A:A)(l:List A),List A.
> > > > >
> > > > > My question is if I can always do it.
> > > >
> > > > Ah, I see.  None of your code above uses "parameters," following 
> > > > official Coq terminology; that only applies to this sort of argument 
> > > > binding at the level of an inductive definition, not a constructor.
> > > >
> > > > However, the first kind of constructor type shorthand notation you 
> > > > demonstrate above _is_ general enough to work for all constructor 
> > > > types. Of course, one of the constructor arguments (or the result) 
> > > > might itself have a [forall] type, in which case you need to get the 
> > > > [forall] in there somehow; none of the shorthands you've shown will 
> > > > help avoid that.