Hi,
I don't know of any function in HOL Light (although I'm don't know about
most recent versions).
To write your own, a simple approach would be to print primitive term
syntax, with all constants and variables annotated with their type, and
to put parentheses around everything at every level. This would be
unreadable for anything but small terms, but would parse back in.
However, even this would have its problems:
(1) If you have generated type variables (e.g. `:?20147`) then HOL Light
cannot parse these back in;
(2) Any irregular names of constants and variables would cause problems
for the parser;
(3) Variables overloaded with constants would not get parsed properly.
But I suppose you are assuming that the original term was successfully
parsed in by HOL Light's parser. If so, then only (1) is a problem.
Mark.
But other if you are not concerned about type variables,
On 29/06/2018 15:26, Yaqing Jiang wrote:
Hi,
Anyone knows if there is a function in HOL Light that convert terms to
strings so that I can save the term and load it the next time?
If I do string_of_term `x:num` I only got "x", but I need "x:num". If
there's none I'll make one myself anyway.
Thanks
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
