Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • From: Éric Tanter <etanter AT dcc.uchile.cl>
  • To: Clément Pit-Claudel <cpitclaudel AT gmail.com>
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] show proof at each step
  • Date: Thu, 25 May 2017 22:14:09 -0400
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=etanter AT dcc.uchile.cl; spf=Pass smtp.mailfrom=etanter AT dcc.uchile.cl; spf=None smtp.helo=postmaster AT sunsite.dcc.uchile.cl
  • Ironport-phdr: 9a23:UnPZgxxwGPKDGF/XCy+O+j09IxM/srCxBDY+r6Qd2usUIJqq85mqBkHD//Il1AaPBtSFra8bw6qO6ua7CDNGuc7A+Fk5M7VyFDY9yv8q1zQ6B8CEDUCpZNXLVAcdWPp4aVl+4nugOlJUEsutL3fbo3m18CJAUk6nbVk9Kev6AJPdgNqq3O6u5ZLTfx9IhD2gar9uMRm6twvcu80XjId4Kqs8yAbCrn9Ud+hL329lK1aekhTm6sus4JJv9jlbtu48+cJHTaj1cKM0QKBCAjghL247+tDguwPZTQuI6HscU2EWnQRNDgPY8hz0XYr/vzXjuOZl1yaUIcP5TbYvWTS/9KhrUwPniD0GNzEi7m7ajNF7gb9BrxKgoxx/xJPUYJ2QOfFjcK7RYc8WSGxcVctKSSdPHp2zYJcOD+oZPOZXsY/9p0cVrRCjAQWgHf7jxiNUinPz26AxzuYvHhzc3AE4A90Bv2naotX3O6kcXu67z6fIwyvEYf5NxTf98Y3Ifgwhof2QX799d9fax0k1FwPCi1WdsZDgPymU1usRq2eV8fBvVeSzi2E5sQF6vz+iydkwiobTgIIV1k7L9T9izYkoOdK3VFR3YcO4H5tQtiGaM5V5Ttk+TGFsoSs3zKANt5C8fCgP0psnxhjfZuSdfIiT/h3jVeeRITFmi3JgYr2znRGy8VKvyuHkTMm7zktFoTdEktnQrHwCyxvT6s2BR/Bg/UmhwS6C2x7P5u1YO0w4i6jWJ4Q/zrMyjJYfrEDOEy3ulEnokKOaal8o9+a05+j9fLnrqJuRO5Vphgz/PKkjnNG0D/4iPQgURWeb/Pyx1L398k39R7VHluY2krTfsJDBJMQburC2DxVI3Yk/9xmzFSqm38gYnXkGKFJKZgiLgJTtO13WIfD4C+mwg0i0nTt12/zKIqftDovPI3TZjrvsf6xx51NYxQcx1dxf4ohbCrAFIPL9QE/xs9nYAwcnPAyo2ennDsl92Z0EWW+UH6CWLL/dvUWV5u0zI+mMZYsVtyjnJ/c54/7ilWU5lkMFfam1wZsXb2i1EehhI0WAeHbjntMBEXoRsQclV+zriFiCUSZJaHqoXqI84Cs7CIO8AovZSICtmu/J4CDuNZnXY21AFme0EGutXIGNRvsBbGrGKddgjjcAXKWtRosJ2hSntQu8wL1ieLn64Cod4DP51dNC2+TViRwovWh5E82bz2yXZ21/lSUVTD832K05qkgrmQTL6rRxn/ENTY8b3PhOSApvcMeEl+E=

> On May 25, 2017, at 9:01 PM, Clément Pit-Claudel
> <cpitclaudel AT gmail.com>
> wrote:
> […]
> If you already use Proof General and company-coq,


of course I use Proof General and company-coq, what else is there?? ;-)))

> There's a demo at
> https://www.reddit.com/r/dependent_types/comments/3ydylj/incremental_program_construction_in_coq/
> (https://asciinema.org/a/bb3fxq5k9cdekaxnb07owf4gn) (though that one shows
> extraction, not partial proof, but it works the same).

brilliant!! I’ll give it a try asap. Thanks (again) for your great work on
company-coq!

— Éric


Archive powered by MHonArc 2.6.18.

Top of Page