coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Notation for Hoare logic

From: Adam Chlipala <adamc AT csail.mit.edu>
To: "Benjamin C. Pierce" <bcpierce AT cis.upenn.edu>
Cc: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Notation for Hoare logic
Date: Fri, 08 Mar 2013 15:50:57 -0500

On 03/08/2013 03:23 PM, Benjamin C. Pierce wrote:

I do want to stay with ascii, to avoid forcing too many people to struggle
with how to edit unicode. But the other solutions do seem pretty reasonable
-- my current favorite is [{P} c {Q}]. Another option we're considering is
to keep {{P}}c{{q}} but fix up the HTML output so that the braces come out
close together.

Can you use coqdoc's "printing" command to render "{{" as "{" in HTML, etc.?

[Coq-Club] Notation for Hoare logic, Benjamin C. Pierce, 03/08/2013
- Re: [Coq-Club] Notation for Hoare logic, AUGER Cédric, 03/08/2013
  - Re: [Coq-Club] Notation for Hoare logic, Benjamin C. Pierce, 03/08/2013
    - Re: [Coq-Club] Notation for Hoare logic, Adam Chlipala, 03/08/2013
      - Re: [Coq-Club] Notation for Hoare logic, Benjamin C. Pierce, 03/08/2013
    - Re: [Coq-Club] Notation for Hoare logic, AUGER Cédric, 03/08/2013
- Re: [Coq-Club] Notation for Hoare logic, CJ Bell, 03/09/2013
  - Re: [Coq-Club] Notation for Hoare logic, CJ Bell, 03/09/2013
    - Re: [Coq-Club] Notation for Hoare logic, Benjamin C. Pierce, 03/23/2013