coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Similarities between forall and fun

From: Yasuaki Kudo <yasu AT yasuaki.com>
To: "coq-club AT inria.fr " <coq-club AT inria.fr>
Subject: [Coq-Club] Similarities between forall and fun
Date: Sun, 15 Nov 2015 12:45:00 +0900
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=yasu AT yasuaki.com; spf=None smtp.mailfrom=yasu AT yasuaki.com; spf=None smtp.helo=postmaster AT mail1.g12.pair.com
Importance: normal
Ironport-phdr: 9a23:bgW7tB0IASxKccIQsmDT+DRfVm0co7zxezQtwd8ZsegQIvad9pjvdHbS+e9qxAeQG96LtrQZ16GP4vCocFdDyKjCmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TWM5DIfUi/yKRBybrysXNWC0oLqi6vrqs2bSj4LrQT+SIs6FA+xowTVu5teqqpZAYF19CH0pGBVcf9d32JiKAHbtR/94sCt4MwrqHwI6LoX0clhfe26Jvx5HvRkC2FsOGcsocbvqBPrTA2V53JaXH9e2FIcCA/cqRr+Q53Zsy3gt+M71jPMbuPsSrVhaD258q5oSVfLlSsAf2oo+XrKot15l79SoxPnrBt6ld2HKLqJPeZzK/uONegRQnBMC58JWg==

Hi,

I’m currently studying COQ (well taking a long time…) and have noticed similarities between forall (dependent product?) and function terms.

Although I understand they are different 😊, I wonder, in other languages or other implementations of similar ideas, can these expressions (universal quantification?) be combined as something unified?

Parameter F : nat -> Set .

Parameter t : forall x:nat , F (1+x) .

Definition t':= fun x:nat => F (1+x).

Check t 1.

Check F (1+1).

Check t' 1.

Regards,

Yasuaki

Tokyo

[Coq-Club] Similarities between forall and fun, Yasuaki Kudo, 11/15/2015
- <Possible follow-up(s)>
- Re: [Coq-Club] Similarities between forall and fun, Kyle Stemen, 11/15/2015
- Re: [Coq-Club] Similarities between forall and fun, Gabriel Scherer, 11/15/2015
  - Re: [Coq-Club] Similarities between forall and fun, effectfully, 11/15/2015
    - 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