The Coq mailing list

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

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.
Regards
Patricia
----- 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:12 PM
Subject: Re: [Coq-Club] parameter


> It's certainly true that such parameter declarations act as implicit 
> binders for the parameter variables, across the whole rest of the 
> inductive definition.  The function arrow [->] is a special case of 
> [forall], so the _type_ of your inductive type family will involve 
> [forall], no matter what you do, as long as there are any parameters.  
> By definition, a type family with parameters must have all constructors' 
> types end in instances of that type family applied to exactly the 
> parameter variables.  So, if you used an explicit [forall] in a 
> constructor to bind a different variable to pass as the parameter value 
> at the end of some constructor type, that would be an error.  (Though 
> you may change the parameter values in the _arguments_ of a constructor, 
> just not the _result_ type)
>
> I feel like I'm probably missing the heart of your question, so let me 
> know if I haven't answered it.
>
> Patricia Peratto wrote:
> > I mean by parameter the name of variable together with
> > its type that one puts to the left of the : in  a definition,
> > by example A:Type in
> > Inductive List (A:Type):Type
> > or
> > (A:Type) and (x:A) in
> > Inductive eq (A:Type)(x:A) : A->Type
> ...
> > Is true that with  parameters and -> I don't need forall?
> > or is there a case in which forall is necesary?