coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] Printing strings with newlines inside Coq

From: Andrew Kennedy <akenn AT microsoft.com>
To: Laurent Théry <Laurent.Thery AT inria.fr>
Cc: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] Printing strings with newlines inside Coq
Date: Wed, 27 Mar 2013 10:10:44 +0000
Accept-language: en-GB, en-US

Aha. I knew it was simple. No such thing as escapes in Coq strings – I don’t know what I was thinking!

Cheers

Andrew.

From: Laurent Théry [mailto:Laurent.Thery AT inria.fr]
Sent: 27 March 2013 09:51
To: Andrew Kennedy
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Printing strings with newlines inside Coq

On 03/27/2013 10:31 AM, Andrew Kennedy wrote:

Coq < Open Scope string_scope.

Coq < Example s := "this is one line\n".

s is defined

An ugly fix is to dig into ascii representation :

Definition newline := String (Ascii.ascii_of_N 10) EmptyString.

[Coq-Club] Printing strings with newlines inside Coq, Andrew Kennedy, 03/27/2013
- Re: [Coq-Club] Printing strings with newlines inside Coq, Laurent Théry, 03/27/2013
  - RE: [Coq-Club] Printing strings with newlines inside Coq, Andrew Kennedy, 03/27/2013
    - Re: [Coq-Club] Printing strings with newlines inside Coq, AUGER Cédric, 03/27/2013
  - Re: [Coq-Club] Printing strings with newlines inside Coq, Maxime Dénès, 03/27/2013
- Re: [Coq-Club] Printing strings with newlines inside Coq, AUGER Cédric, 03/27/2013