The Coq mailing list

[Andrew Kennedy <akenn AT microsoft.com>]

Hello

 

I have a seemingly simple problem: I want to pretty-print a large term inside Coq, simply by writing a function

   pretty : Tm -> string

and then be able to compute the string and look at it inside Proof General, or coqtop. But when using “Compute” or “Print” the string remains “within quotes”, and the newlines remain escaped. Example:

 

Welcome to Coq 8.4pl1 (January 2013)

 

Coq < Require Import String.

[Loading ML file z_syntax_plugin.cmxs ... done]

[Loading ML file quote_plugin.cmxs ... done]

[Loading ML file newring_plugin.cmxs ... done]

[Loading ML file ascii_syntax_plugin.cmxs ... done]

[Loading ML file string_syntax_plugin.cmxs ... done]

 

Coq < Open Scope string_scope.

 

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

s is defined

 

Coq < Example ss := s++s++s++s++s++s++s.

ss is defined

 

Coq < Compute ss.

     = "this is one line\nthis is one line\nthis is one line\nthis is one line\n

this is one line\nthis is one line\nthis is one line\n"

     : string

 

 

I want a way of *actually* *printing* the darn thing. Is there a way?

 

(Yes, I have considered simply using Notations for my Tm type, with format specifiers that incorporate line breaks, etc. But sometimes it’s just easier to write a function into string, as one would do in ML or Haskell.)

 

Cheers

Andrew.