The Coq mailing list

[Guillaume Brunerie <guillaume.brunerie AT gmail.com>]

Because it's the same thing.
A proof of the implication A -> B is a function taking a proof of A
and returning
a proof of B.
This identification of a proposition with the type of its proofs
(known as the Curry-Howard correspondence) is very fundamental to Coq
and is probably explained in every Coq tutorial you can find.

Best,

Guillaume

On 2013/9/8 N. Raghavendra 
<raghu AT hri.res.in>
 wrote:
> 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.
>
> --
> N. Raghavendra 
> <raghu AT hri.res.in>,
>  http://www.retrotexts.net/
> Harish-Chandra Research Institute, http://www.hri.res.in/
>