Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] rules for which Unicode symbols may be used in notations

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] rules for which Unicode symbols may be used in notations


chronological Thread 
  • 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


Archive powered by MhonArc 2.6.16.

Top of Page