coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Similarities between forall and fun

From: Freek Wiedijk <freek AT cs.ru.nl>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Similarities between forall and fun
Date: Mon, 16 Nov 2015 12:50:54 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=freek AT cs.ru.nl; spf=None smtp.mailfrom=freek AT cs.ru.nl; spf=None smtp.helo=postmaster AT smtp1.science.ru.nl
Ironport-phdr: 9a23:FW7X0BDZn9H+QOJklwCfUyQJP3N1i/DPJgcQr6AfoPdwSP74psbcNUDSrc9gkEXOFd2CrakU1qyL7Ou7ASQp2tWojjMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpQAbFhi3DwdpPOO9QteU1JTqkb3tsMaLKyxzxxODIppKZC2sqgvQssREyaBDEY0WjiXzn31TZu5NznlpL1/A1zz158O34YIxu38I46FppIZ8VvDxeL19RrhFBhwnNXo07Yvlr0rtVwyKs1UGX2gV2iVJDgTE7hKyCpnrvyb5nuFmnjOHe8vyG+NnEQ++5rtmHUe7wBwMMCQ0pTna

Hi Thorsten,

>What is nice about this conceptual confusion?

That you can get away with it? That you can simplify your
syntax and typing rules that way and still have a viable
logical framework?

The "[x:A]" binder of automath should not be thought of
as creating a function or function type. It is "just"
a notion of binding a variable, to be able to do HOAS.

I'm not saying that the Automath approach to type theory
is more powerful than the "modern" one (it's basically an
alternative to LF), but it _is_ simpler and more regular
and it _does_ work.

Freek

[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
        
        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, Soegtrop, Michael, 11/16/2015