coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: RE: [Coq-Club] Similarities between forall and fun
- Date: Mon, 16 Nov 2015 14:36:58 +0000
- Accept-language: de-DE, en-US
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga11.intel.com
- Ironport-phdr: 9a23:DbjAchcvQ/YCHSzdXqjlmm4glGMj4u6mDksu8pMizoh2WeGdxc69ZR7h7PlgxGXEQZ/co6odzbGG7ua9BideuN6oizMrTt9lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUiv2OQc9HOnpAIma153xjLDvvcCMKFsRzBOGIppMbzyO5T3LsccXhYYwYo0Q8TDu5kVyRuJN2GlzLkiSlRuvru25/Zpk7jgC86l5r50IAu3GePFyRrtBST8iLmod5cvxtBCFQxHFri8XVXxTmR5VCSDE6gv7V9H/qH2pmPB63XzQBsr7QqwuXizmp4JqQx/hhSNNf2o88WrXg8F0yrlcrR29vRtn64/SfIyRcvF5e/WOLpshWWNdU5MJBGR6CYSmYt5XAg==
Dear Yasuaki,
I’m currently studying COQ (well taking a long time…) and have noticed similarities between forall (dependent product?) and function terms.
actually in Coq I would think they are the same, not just similar. It is interesting to look at function types with notation switched off (View Menu in CoqIDE):
Definition add (a b : nat) := a+b. Check add.
With notation switched on, you get this:
add : nat -> nat -> nat
Wit notation switched off, you get this:
add : forall (_ : nat) (_ : nat), nat
Likewise you get for
Lemma add' : forall (a b : nat), nat. intros a b. exact (a+b). Defined. Check add'.
with notations switched on the type
add' : nat -> nat -> nat
So as it looks, in Coq -> is just a notation for forall for cases where the result type does not depend on the arguments.
Best regards,
Michael Intel Deutschland GmbH |
- Re: [Coq-Club] Similarities between forall and fun, (continued)
- Re: [Coq-Club] Similarities between forall and fun, Dominic Mulligan, 11/15/2015
- Re: [Coq-Club] Similarities between forall and fun, Andreas Abel, 11/19/2015
- RE: [Coq-Club] Similarities between forall and fun, Yasuaki Kudo, 11/17/2015
- Re: [Coq-Club] Similarities between forall and fun, Yves Bertot, 11/16/2015
- Re: [Coq-Club] Similarities between forall and fun, Freek Wiedijk, 11/16/2015
- Re: [Coq-Club] Similarities between forall and fun, Thorsten Altenkirch, 11/16/2015
- Re: [Coq-Club] Similarities between forall and fun, Freek Wiedijk, 11/16/2015
- Re: [Coq-Club] Similarities between forall and fun, Thorsten Altenkirch, 11/16/2015
- Re: [Coq-Club] Similarities between forall and fun, Randy Pollack, 11/16/2015
- Re: [Coq-Club] Similarities between forall and fun, Freek Wiedijk, 11/16/2015
- Re: [Coq-Club] Similarities between forall and fun, Freek Wiedijk, 11/16/2015
- Re: [Coq-Club] Similarities between forall and fun, Thorsten Altenkirch, 11/16/2015
- Re: [Coq-Club] Similarities between forall and fun, Freek Wiedijk, 11/16/2015
- RE: [Coq-Club] Similarities between forall and fun, Soegtrop, Michael, 11/16/2015
- Re: [Coq-Club] Similarities between forall and fun, Dominic Mulligan, 11/15/2015
Archive powered by MHonArc 2.6.18.