The Coq mailing list

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

In case of a formation rule, can I replace in an inductive declaration of a 
type a forall
by 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 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.