Re: [isabelle] make_string

On 21/06/18 02:15, Jeremy Dawson wrote:
> Well, obviously I don't want to create a print function for any new
> datatype when there is one there already (now that I've been told how to
> remove all the extra crap in the output from @{make_string}).
> In what way is @{make_string} not suitable for production-quality output?

Before we continue this thread, can you just explain what you are trying
to do.

There is usually no need to abuse Isabelle/ML to get things done properly.


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