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
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
--
The University of Edinburgh
