coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Automatic conversion into a notation

From: Adam Chlipala <adamc AT csail.mit.edu>
To: Victor Porton <porton AT narod.ru>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Automatic conversion into a notation
Date: Fri, 04 Nov 2011 17:10:52 -0400

Victor Porton wrote:

I have the following trouble (not exactly this, but similar):

I have sources (.v) files where the notation (plus A B) abounds.

I want to convert it into a visible format (for example, HTML or PDF) with
all (plus A B) replaced with A+B.

Can this be done easily?

Please see the Coq manual's documentation on the "coqdoc" tool.

[Coq-Club] Automatic conversion into a notation, Victor Porton
- Re: [Coq-Club] Automatic conversion into a notation, Adam Chlipala
  - Re: [Coq-Club] Automatic conversion into a notation, Adam Chlipala
- <Possible follow-ups>
- Fwd: [Coq-Club] Automatic conversion into a notation, Victor Porton
  - Re: Fwd: [Coq-Club] Automatic conversion into a notation, Adam Chlipala