The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Sun, 08 Sep 2013 16:22:18 +0530,
"N. Raghavendra" 
<raghu AT hri.res.in>
 a écrit :

> I'm learning Coq and am wondering why the symbol -> is used both for
> functions between types as in "evenb : nat -> bool", and for
> implications between propositions as in "forall n : nat, even n ->
> even (S (S n))".  Is there any mathematical reason for this, or is it
> just a matter of convenience?
> 
> Best regards,
> Raghu.
> 

And also, remember that in Coq, "A -> B" is just a notation for
"forall (_:A), B".

I do not remember if starting the session with "-nois" parameter
triggers an error when you write "A -> B".