coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Lean Theorem Prover

From: "John Wiegley" <johnw AT newartisans.com>
To: Freek Wiedijk <freek AT cs.ru.nl>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Lean Theorem Prover
Date: Thu, 25 Feb 2016 14:31:40 -0800
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jwiegley AT gmail.com; spf=Pass smtp.mailfrom=jwiegley AT gmail.com; spf=None smtp.helo=postmaster AT mail-pf0-f172.google.com
Ironport-phdr: 9a23:f46bChCQ5gF7/2nPUjpuUyQJP3N1i/DPJgcQr6AfoPdwSP/5psbcNUDSrc9gkEXOFd2CrakU1KyI6eu4ACQp2tWojjMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpQAbFhi3DwdpPOO9QteU1JTokb7osMWKKyxzxxODIppKZC2sqgvQssREyaBDEY0WjiXzn31TZu5NznlpL1/A1zz158O34YIxu38I46Fp34d6XK77Z6U1S6BDRHRjajhtpZ6jiR6WYxGC63hUbWQbnhtKAECR4gv3U5TZuTC8rPc73i3Mbvf7VbQlZTP3pYVsSBmgtyYKODo04Suf3s53jKREiBSsuBVl34/PaYeOcvF5e/WOU8kdQD8LfMFRUWR+A46za4YeRaJVP+FYqZbVoVYRpAGiBBKlAvipwThN0CyllZYm2vgsRFmVlDcrGMgD5TGN9I34
Organization: New Artisans LLC

>>>>> Freek Wiedijk
>>>>> <freek AT cs.ru.nl>
>>>>> writes:

> The type theory is simpler: they don't have "match" in the foundations, but
> instead work with recursors

I wonder if runs into the same issues that Coq did. See "Meta-theory à la
Carte", section "The Problem of Church Encodings and Induction",
http://people.csail.mit.edu/bendy/MTC/.

--
John Wiegley GPG fingerprint = 4710 CF98 AF9B 327B B80F
http://newartisans.com 60E1 46C4 BD1A 7AC1 4BA2

RE: [Coq-Club] Lean Theorem Prover, (continued)
- Re: [Coq-Club] Lean Theorem Prover, Daniel Schepler, 02/25/2016
  - Re: [Coq-Club] Lean Theorem Prover, Abhishek Anand, 02/25/2016
    - Re: [Coq-Club] Lean Theorem Prover, Daniel Schepler, 02/26/2016
      - Re: [Coq-Club] Lean Theorem Prover, roux cody, 02/26/2016
        
        Re: [Coq-Club] Lean Theorem Prover, Jonathan Leivent, 02/26/2016
        
        Re: [Coq-Club] Lean Theorem Prover, Arnaud Spiwack, 02/26/2016
        
        Re: [Coq-Club] Lean Theorem Prover, Clément Pit--Claudel, 02/26/2016
        
        Re: [Coq-Club] Lean Theorem Prover, Benjamin C. Pierce, 02/26/2016
        RE: [Coq-Club] Lean Theorem Prover, Soegtrop, Michael, 02/26/2016
        Re: [Coq-Club] Lean Theorem Prover, Clément Pit--Claudel, 02/26/2016