Re: [isabelle] make_string



On 20/06/18 15:04, Jeremy Dawson wrote:
> 
> Thanks for the information that I shouldn't be using @{make_string}.
> This raises the obvious question of what I should be using.  Would it be
> possible for you to tell me that?  Ie, what is the equivalent in the
> managed ML environment called "Isabelle/ML" of the PolyML function
> PolyML.makestring?

There is none. For quick adhoc debugging and diagnistics, there is
@{print} and @{make_string}. For production-quality output, you do it
yourself specifically for your data types, potentially using existing
operations like Syntax.pretty_term -- generally it is better to print
Pretty.T than string.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.