coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Same symbol for functions and implication

From: "N. Raghavendra" <raghu AT hri.res.in>
To: coq-club AT inria.fr
Subject: [Coq-Club] Same symbol for functions and implication
Date: Sun, 08 Sep 2013 16:22:18 +0530
Cancel-lock: sha1:aX0EYrGxgxmlX7VDzRz7hFH1yME=

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/

[Coq-Club] Same symbol for functions and implication, N. Raghavendra, 09/08/2013
- Re: [Coq-Club] Same symbol for functions and implication, Guillaume Brunerie, 09/08/2013
  - [Coq-Club] Re: Same symbol for functions and implication, N. Raghavendra, 09/09/2013
- Re: [Coq-Club] Same symbol for functions and implication, Daniel de Rauglaudre, 09/08/2013
- Re: [Coq-Club] Same symbol for functions and implication, AUGER Cédric, 09/08/2013
  - Re: [Coq-Club] Same symbol for functions and implication, Arnaud Spiwack, 09/09/2013