Dear experts,
Let’s say I create a new variable in the c++ interface:
PlTerm t ;
When I print this variable, e.g. by
cout << (char*) t << endl ;
It’s name is something like _1620. Can I give it a different name? I need it for pretty printing only, so, in principle, I can unify it with some atom ‘X’ and all good, but maybe there is something more elegant.
Best wishes
Matthias