coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] show proof at each step

From: Clément Pit-Claudel <cpitclaudel AT gmail.com>
To: Éric Tanter <etanter AT dcc.uchile.cl>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] show proof at each step
Date: Thu, 25 May 2017 22:34:51 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=cpitclaudel AT gmail.com; spf=Pass smtp.mailfrom=cpitclaudel AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt0-f170.google.com
Ironport-phdr: 9a23:51hv6RBEkfSAtw2SPBSiUyQJP3N1i/DPJgcQr6AfoPdwSPX7pcbcNUDSrc9gkEXOFd2CrakV1ayL7OigATVGusfe9ihaMdRlbFwst4Y/p08aPIa9E0r1LfrnPWQRPf9pcxtbxUy9KlVfA83kZlff8TWY5D8WHQjjZ0IufrymUoHdgN6q2O+s5pbdfxtHhCanYbN1MR66sRjdutMYjIZmK6s90BvEr3lVcOhS2W9kOEifkhj468qy5pJv7zhct/c8/MNcTKv2eLg1QrNfADk6KW4549HluwfeRgWV/HscVWsWkhtMAwfb6RzxQ4n8vCjnuOdjwSeWJcL5Q6w6VjSk9KdrVQTniDwbOD4j8WHYkdJ/gaRGqx+8vRN/worUYIaINPpie67WYN0XSXZdUstXSidMGZ23YZcRAOUdPOZYt4j9qEUIrRuiHgmnGefjxiZVinPqwaE21uIsGhzE0gM9BdIDqHTaosjrOqccUu67wqfHwjrBYPxK1jnw85TIfxM7rP2QQb59f8jcxE8yHA3FlFWQronlMiuL2+QJqW+b6vRvVeSzi2E/sQ9xoySvyt4yh4nNnI0V103L+jt9wI0oItC3VFZ7Yd+4EJRMsyGVLZZ2Td48TGFsoys6xbgGtoS6fCgO0pgo2xnfa/mefoWO/xntWuGRITJii3JkfrKynxOy8Um8yuHmSMa7zUtKoyxYmdfPrnAAzwLf5tSDR/dn/Uqs2SyD2x7O5uxFO0w4iKjWJ4I5zrItlZcfq1nPEyzylUnskaObdF8o9vWo5unmZLjtu4WSOJVuig7kN6Qjgsy/Dvo8MggJR2Wb/P6z1Lzn/UHgWbVKkuE6nrDXsJzHJ8kXurS1AwBS0oYk5Ba/Cymp3M4EknkAKVJJYBOHj473NFHSOP30E+uzjlC2nDpox/3KJKPtDojMI3TZjbvsf6px51ZZyAUpzNBf45xUCqsGIPL2QkL+qMTYDh4lMwOox+boEsh92Z4AVmKLGaKZP6bSvkWJ5uIrOeWDeIgVuDPlJ/g/+/HulWM5mUMafaSxwZQXb2m4Eu16LEWdfHrjmcwMEXwKvwo7VOzlkkeOUT9VZ3aoXqIz/Cs3CIy8DdSLeof4IaaA1xCHF5tKa3oOXl2QGHH0ep+sV/wHLj+ZIs5ln3oPUe7yZZUm0ESFsI7/xrx7GdLV5mgzsZv+2NVxr7nYjRAu/jh9EsiQ10mCSmh1miUDQDpgj/M3mlB01lrWifswuPdfD9EGoqoRCgo=

On 2017-05-25 22:14, Éric Tanter wrote:
> brilliant!! I’ll give it a try asap. Thanks (again) for your great work on
> company-coq!

Cool :) There's an example file in that same folder.
Here's a gif: http://web.mit.edu/cpitcla/www/term-builder.gif

[Coq-Club] show proof at each step, Éric Tanter, 05/26/2017
- Re: [Coq-Club] show proof at each step, Jason Gross, 05/26/2017
  - Re: [Coq-Club] show proof at each step, Clément Pit-Claudel, 05/26/2017
    - Re: [Coq-Club] show proof at each step, Éric Tanter, 05/26/2017
      - Re: [Coq-Club] show proof at each step, Clément Pit-Claudel, 05/26/2017
        
        Re: [Coq-Club] show proof at each step, Éric Tanter, 05/26/2017