coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Éric Tanter <etanter AT dcc.uchile.cl>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] show proof at each step
Date: Thu, 25 May 2017 22:42:38 -0400
Authentication-results: mail3-smtp-sop.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:vfx2xB2brBWnDeWSsmDT+DRfVm0co7zxezQtwd8ZseIXK/ad9pjvdHbS+e9qxAeQG96KtbQZ1KKW6/mmAj1fp87Z8TgrS99laVwssYYso0QYGsmLCEn2frbBThcRO4B8bmJj5GyxKkNPGczzNBX4q3y26iMOSF2kbVImbuv6FZTPgMupyuu854PcYxlShDq6fLh+MAi6oR/fu8QSgIZuMKY8xxnUqXdMZ+ha2HlkKFyXkhv+/Mu84IJv/yFNsP896sBMVrn3cKs/QbFEFjoqNHw76tP2vhfZVwuP4XUcUmQSkhVWBgXO8Q/3UJTsvCbkr+RxwCaVM9H4QrAyQjSi8rxkSAT0hycdNj4263/Yh8pth69Guh2hphh/w4nJYIGJMfd1Y63Qcc8GSWdHQ81cUTFKDIGhYIsVF+cOIelXoZT9qVQMoxWwCgqiBO3xxDFPnXL2wbQ60+E9HQHGwAAtHdQDu2nUotXvM6cSVPi4ybXSzTXCc/xZwSnz55LOchA9v/6MR697fM3PxkkzDQzFiEmQppL/Pz6Oy+sCr3SU4/B9Ve2zi24nqgVxrSa1ysgwjonEn4QYwU3K+yV+xYY6P9y4SEhjbN6hEZtQqzuWOJVrTcM/RWxjpSU0yqUetJKlYCQG1I4rywDdZvCdbYSF4AjvWPuVLDp6nH5pZq6ziwqo/UWu1uHwTNe43VhOoyZfj9XBt34A2hrO4cadUPR95F2u2TOX2gDT9O5EJUc0mLLAK548xL4wjZsTsVjdESPshUr5kLOZel85+ue06+TnY7HmqYGGO4BojgHyKqUumsqhDuQkKgUCQXSX9fim2LH9/0D1WqtGg/8snqXEtJ3XJ9wXpqujDA9U1oYj5Qy/DzCj0NkAg3YHMEhKeBSbj4f3IVHDO+33AuujjFi2jTdk2/DGPrzlAprTNHTMjLPhca5n60FA0Aoz0cxf55VMB74dJ/LzQ1b9u8DcDh8kKAO52P3nCdV41oMGQ22DGK6ZMKXIsV+J/O0jOeeMZJVG8Ar6fvMi/rvliWIzsV4bZ6igm5UNO16iGfEzgl+Yak3Qi9EdHH1C6gciRer2hUeqXTVYIWu5X6M463cwDNT1Xs/4WomxjenZj2+AFZpMazUeBw==

Ok, I just installed it now and tried it, it works like a charm. I believe my
students will be very grateful ;-)

— Éric

> On May 25, 2017, at 10:34 PM, Clément Pit-Claudel
> <cpitclaudel AT gmail.com>
> wrote:
>
> 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