coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] "Lean is like Coq but better"

From: Bas Spitters <b.a.w.spitters AT gmail.com>
To: Kevin Buzzard <kevin.m.buzzard AT gmail.com>, Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] "Lean is like Coq but better"
Date: Thu, 2 Jan 2020 18:35:21 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=b.a.w.spitters AT gmail.com; spf=Pass smtp.mailfrom=b.a.w.spitters AT gmail.com; spf=None smtp.helo=postmaster AT mail-yw1-f47.google.com
Ironport-phdr: 9a23:iHJg1h2GDMlSSInasmDT+DRfVm0co7zxezQtwd8ZseIeK/ad9pjvdHbS+e9qxAeQG9mCsLQe17Od6vi5EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCezbL9oMhm7ohjdusYLjYd+N6o61wfErGZPd+lK321jOEidnwz75se+/Z5j9zpftvc8/MNeUqv0Yro1Q6VAADspL2466svrtQLeTQSU/XsTTn8WkhtTDAfb6hzxQ4r8vTH7tup53ymaINH2QLUpUjms86tnVBnlgzocOjUn7G/YlNB/jKNDoBKguRN/xZLUYJqIP/Z6Z6/RYM8WSXZEUstXSidPAJ6zb5EXAuUOPehWoYrzqUYQoxSiHgSsGP/jxyVUinPqwaE30eIsGhzG0gw6GNIOtWzZocjvO6cJTOu70bHIzTTfb/NKxzj98pPIeQ0mrP6XR75/a9DdyEc1GwPellWQqJDlPy+L2eQXqGiW9OVgVee1hG4mrwF9uCSgxsApioTQgI8e117K9SJ8wIkvJN24TlZ2Yd+hEJtIqS6aLYp2TdkmQ21yoik11qcKuYO4fCQS1JsnwgPfZ+aZfIeV/xLuUvuaLzRghH99Zr6zmxK//VKjx+D8TMW4zVdHojdfntTDtH0A0QHY5NKdRftn5Eih3C6C1wDN5eFAJkA5ja/bJIQgwr40j5YSsUrCEjLvlEX4g6KbdF8o+uev6+TgbbXmooGTO5VohQH5N6Qigs2/AeImPQgSR2WX5/iw2bn58UD6QLhGlOA6n6jEvJzAKskWpLa1AwpP3YYi7xa/AS2m0NMdnXQfN11JYgiIg5LnOl3UO/D4Ffa/g0iwkDh13fDGJabsAprILnfZkbfheaxx5FJbyAo21dxf/Y5bCqkdIPLvXU/8rMDXDhggMwCt3+nnDMh92ZgFVGKUAq6ZNbvSvkWS6uIuJemMfo4VtyznJ/gr/f69xUM+zHwQY6ivlbEKemKxBPgud0aUf3vqxNJHG3oYrAMkQMTljVSDVXhYYHPkG+oX4ShzI4a7B8+XTYe0xbeFwS2TH5tMZ2kABEraQlnycIDRcf4XIBmKI9N9nyYfHeyrDYZnyle1rA7m17d9NcLb/yQZsdTo090jtL6brg076TEhV5fV6GqKVWwh2zpQH2ZqjpA6mlR0zxK46YY9m+ZRTIUB6PZAUwN8PpnZnbQjVoLCHznZd9LMc26IB9WrBTZrE4A0yt4KJldiQpCs0k+F0C2tDLsY0beMAc5sq/OO7z3KP894jk3++uwkhlgiTNFIMDT/1KF6/gnXQYXOlhfAmg==

Dear Kevin,

You claimed
"Lean is like Coq but better"
https://wwwf.imperial.ac.uk/~buzzard/one_off_lectures/msr.pdf

There was a bit of discussion among coq users about what this means.
Did you have any concrete suggestions on how lean is better, and how
Coq could be improved?

While I'm at it, let me announce this workshop next week to the coq-community:
https://www.andrew.cmu.edu/user/avigad/meetings/fomm2020/

Best regards,

Bas

[Coq-Club] "Lean is like Coq but better", Bas Spitters, 01/02/2020
- Re: [Coq-Club] "Lean is like Coq but better", Timothy Carstens, 01/02/2020
  - Re: [Coq-Club] "Lean is like Coq but better", Kevin Buzzard, 01/02/2020
    - [Coq-Club] Fwd: "Lean is like Coq but better", Kevin Buzzard, 01/02/2020
      - Re: [Coq-Club] Fwd: "Lean is like Coq but better", Gaëtan Gilbert, 01/03/2020
        
        Message not available
        
        Re: [Coq-Club] Fwd: "Lean is like Coq but better", Ramkumar Ramachandra, 01/04/2020
        
        Re: [Coq-Club] Fwd: "Lean is like Coq but better", Bas Spitters, 01/06/2020
        Re: [Coq-Club] Fwd: "Lean is like Coq but better", Kevin Buzzard, 01/06/2020
        Re: [Coq-Club] Fwd: "Lean is like Coq but better", Conor McBride, 01/06/2020
        
        Re: [Coq-Club] Fwd: "Lean is like Coq but better", Stefan Monnier, 01/06/2020
        
        Re: [Coq-Club] Fwd: "Lean is like Coq but better", Bas Spitters, 01/06/2020