coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] show proof at each step

From: Éric Tanter <etanter AT dcc.uchile.cl>
To: coq-club AT inria.fr
Subject: [Coq-Club] show proof at each step
Date: Thu, 25 May 2017 18:23:06 -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:HOP9ABbP3k9v6GOzY+yN51n/LSx+4OfEezUN459isYplN5qZoMu5bnLW6fgltlLVR4KTs6sC0LuI9f2/ESxYuNDa4S9EKMQNHzY+yuwo3CUYQ/S5QXXhK/DrayFoVO9jb3RCu0+BDE5OBczlbEfTqHDhpRQbGxH4KBYnbr+tQt2agMu4zf299IPOaAtUmjW9falyLBKrpgnNq8Uam4VvJ6IwxxfTonZFefldyWd0KV6OhRrx6MO98Zx5/yhMp/4t8tNLXLnncag/UbFXAzMqPnwv6sHsqRfNUxaE6GEGUmURnBpIAgzF4w//U5zsrCb0tfdz1TeDM8HuQr86RTqt76FwSB/1kygHLCI28HvWisNrkq1Wpg+qqgFlzI7VZIGVM+d+fr/YcNgHS2dNQtpdWipcCY66coABDfcOPfxAoof9u1QAogawCwqiCu3xxTBGgWT73bEj0+QkDQ3G3BAsEtAIvX/JrNv1LqASUeWtwazU1zXDbu9Z1i/j5ofSdBAhve+DXahtesfW10YvCxnKjlOMqYP7JTOYzfkCvHSH4OZ6SOKgl24nqwB1ojex3Msjlo3Ji5sTx1vZ9it52J44KcOkREJne9KoDplduzuEO4Z0WM8uXmVltSQixrEbvZO3YjIGxZc7yxLFdfCKfJKE7g/hWeuRJzpzmWhrd6ilhxmo9Eit0u38Wdew0FZNtidFicTMtnYW1xzS9siIVOFx8Vq91jmTzQzT9/1LIUA1larfNZEt2KI/lp4LvUTCGC/5hln2gbeIekk45uSk8frrb7f8qpOCNYJ4kBzyP6Asl8CnBOQ3KAkOX2yV+eSm073j+FX0T6tWjvIslKnZrI7VJd4Aq6GkHwBazpwv6wujADem0dQYmWcIIEhZdxKDl4TpIU3BIOjkDfejhFShiCtkx/ffPrH4HprNKmXDn6z6cLZm609czRIzwspF65JVDLEBOvPzVVXruNzWFB9qezCzlu3gEZB20p4UcWOJGK6Qdq3I4nGS4ed6gvONb7gpsTDhJuJts/PyhHkllEU1caKim4YcaHG8E7JtJxPKMjLXnt4dHDJS7UIFR+vwhQjaXA==

Hi,

When writing a proof, one can use “Show Proof” to display the current term in
the response pane. This can be really helpful.
So much that I’d like to be able to turn it on at all steps, in order to
follow the step-by-step construction of the term without having to write down
“Show Proof” after each dot.
I understand that in general it is not practical for efficiency reasons, but
as a pedagogical tool it would be great to have so that students “see” the
term being built.

Is there a way to (locally) activate “Show Proof” for each step of the term
construction?

Thanks,

— Éric

[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