The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

Hi,

On Thu, Apr 02, 2009 at 04:04:52PM +0100, Ian Lynagh wrote:
> On Thu, Apr 02, 2009 at 04:53:40PM +0200, Guillaume Melquiond wrote:
> > 
> >         Require Import String.
> >         (* Definition my_string := "*)"%string. *)
> >         Definition my_string := "let's try something else"%string.
> 
> Perhaps (* and *) should not be allowed in string literals.
> You would have to write
> 
> Definition my_string := "*" ++ ")"%string.
> 
> instead (or whatever string append looks like in coq). Or in Haskell,
> you could write it as, for example, "*\&)" or "\42)"; I don't know if
> coq has a similar syntax.

You can do things like that by concatening strings and chars:

Require Import Ascii String.
Coercion of_char s := String s EmptyString.
Open Scope string_scope. 
Definition msg := Eval compute in 
  "040"%char ++ "* Hello! *" ++ "041"%char ++ "010"%char.
Print msg.

Alternatively, nothing forbids to write an interpreter of strings that
interprets strings as you want (as long as you comply with the
convention that a doubled double-quotes internally denotes a single
double-quotes).

Hugo Herbelin