The Coq mailing list

["N. Raghavendra" <raghu AT hri.res.in>]

At 2013-09-08T12:59:30+02:00, Guillaume Brunerie wrote:

> 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.

Thanks for the reply.  I should get around to reading about the
Curry-Howard correspondence seriously.  Will come back here if I've
questions there.

Best regards,
Raghu.

-- 
N. Raghavendra 
<raghu AT hri.res.in>,
 http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/