coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: David MENTRE <dmentre AT linux-france.org>
- To: "Benjamin C. Pierce" <bcpierce AT cis.upenn.edu>
- Cc: Adam Megacz <megacz AT cs.berkeley.edu>, coq-club AT inria.fr
- Subject: Re: [Coq-Club] rules for which Unicode symbols may be used in notations
- Date: Wed, 6 Oct 2010 20:26:49 +0200
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:from:date :x-google-sender-auth:message-id:subject:to:cc:content-type :content-transfer-encoding; b=VwIfN0SjdlrkQTV4vegzBC2fMVtuyN9ao9Dlput/v+bGeVa1Ngd2CGa3NRNUXoCTBc OGg2VOxgksO2vi1+VSDEOuvpZNRaDEiX2Fjj5oITFIPEXRbm4CiI588wOJkmWBiFlGoB mwfLWbbFbO4CA7qaP4EIwzNltGgfySxIyzQI4=
Hello,
2010/10/6 Benjamin C. Pierce
<bcpierce AT cis.upenn.edu>:
> Not in itself, but it's an aspect of an issue that's becoming more
> important over time: in general, Coq's notations are not nearly as nice to
> look at as, say, Isabelle's. Doesn't matter so much in day to day theorem
> proving work, but it becomes more of a problem when Coq proofs get shown to
> students or used in publications.
Regarding publications supposedly done with LaTeX, I would recommend
to look at the "listings" LaTeX package[1]. It has a "literate
programming" functionality (see §5.4) that allows to easily substitute
LaTeX symbols to ASCII ones. I use it heavily to include pieces of
another formal notation (B Method) into documentations and articles.
Sincerely yours,
D. Mentré
[1] ftp://ftp.tex.ac.uk/tex-archive/macros/latex/contrib/listings/listings.pdf
- [Coq-Club] rules for which Unicode symbols may be used in notations, Adam Megacz
- Re: [Coq-Club] rules for which Unicode symbols may be used in notations,
Benjamin C. Pierce
- Re: [Coq-Club] rules for which Unicode symbols may be used in notations, David MENTRE
- Message not available
- Re: [Coq-Club] rules for which Unicode symbols may be used in notations,
Benoît Montagu
- Re: [Coq-Club] rules for which Unicode symbols may be used in notations, Christian Doczkal
- Re: [Coq-Club] rules for which Unicode symbols may be used in notations,
Benjamin C. Pierce
- Re: [Coq-Club] rules for which Unicode symbols may be used in notations, Pierre Letouzey
- Message not available
- Re: [Coq-Club] rules for which Unicode symbols may be used in notations,
Benoît Montagu
- <Possible follow-ups>
- Re: [Coq-Club] rules for which Unicode symbols may be used in notations, Hugo Herbelin
- Re: [Coq-Club] rules for which Unicode symbols may be used in notations,
Benjamin C. Pierce
Archive powered by MhonArc 2.6.16.