The Coq mailing list

[Maxime Dénès <Maxime.Denes AT inria.fr>]

Hello Andrew and Laurent,

Maybe the same trick can have a slightly less ugly presentation:

Definition newline := String "010" "".

However, there are at least three drawbacks to this:
  - The quotes are still surrounding the whole string, which is even 
uglier when newlines are displayed.
  - The newline character is hard-coded and hence not portable (e.g. 
Unix-like versus Windows systems).
  - It does not provide a way to define a real printing function, that 
could display any intermediate result during a computation (e.g. for 
debugging purposes). Instead, the whole function you evaluate has to 
return a String.

An alternative approach would be to have a "print" function as a 
primitive in the calculus, behaving like identity except that its 
reduction would trigger the display of its argument as a side effect. 
Printing inside Coq would then be very close to OCaml, and would 
probably allow a more flexible pretty printer for strings.

I think this question was raised at some point during the discussion on 
"computation inside Coq" of Coq workshop 2012. I'm currently working on 
adding some primitive operators inside Coq on integers and arrays, and 
I'll try to see what can be done for strings as well.

Even in the current context, maybe the syntax plugin for strings could 
recognize escapes.

Best,

Maxime.


On 27/03/2013 10:51, Laurent Théry wrote:
> 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.