Re: [isabelle] make_string



 And just like @{make_string} combined with |> YXML.parse_body |>
XML.content_of seems to do, but you seem to be saying that I shouldn't
use this for production-quality output (why is this the case?)

I would be suprised if that worked for terms.

If you use this routine on the term "λx. x", you'll get:

  Abs ("x", "'a", Bound 0)

Note that the type there is pretty-printed as "'a". If you try to read that in in an ML block:

  ML‹Abs ("x", "'a", Bound 0)›

You'll get an error message that the type is supposed to be a "typ", not a "string". The correct ML input representation would instead be:

  Abs ("x", TFree ("'a", ["HOL.type"]), Bound 0)

I would instead recommend dealing with non-human-readable terms in files instead (arguably, the above is not really human-readable anyway).

Cheers
Lars




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