Re: [isabelle] make_string



Hi,

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

You will not get this from @{make_string}, only something similar looking
but unparseable.
@{make_string} gives you somewhat human readable output, for debugging
(which, in case of term is relatively raw, I assume that is because it has
to work on non-wellformed terms, too).
So - independent of whether it is production-suitable or it - it does not
seem to be what you are looking for.

If I understand right, what you want is something that converts a term into
valid ML-code?
You find this here: ML_Syntax.print_term

I think the reason why @{make_string} is not production-suitable (besides
the fact that for terms, it is not very readable) is that it is a bit of a
hack: It does not have an argument "context", so it has to guess which
context is appropriate for the term at hand.

Best wishes,
Dominique.



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