[opentheory-users] Type variable names

[Rob Arthan]

I have a problem with edge cases in the mappings of type variable
names. What currently happens is that I export them as they stand
and import them by prefixing them with a prime if they don't already
start with one. Ramana does something more complicated by also 
converting a primed single letter to upper case on output and to
lower case on input. The upshot of this is 'a in ProofPower imports as 'a
in HOL4 which then imports back into ProofPower as 'A which imports
back into HOL4 as 'a and now we are in a loop. This is harmless
but a bit silly. So should I be adjusting the case like Ramana does?
And if so why?

Since a HOL4 or ProofPower theory with non-standard type variable
names looks a mess and since the Gilith OpenTheory Repo seems
to have standardised on what HOL4 and ProofPower consider
non-standard, these mappings are necessary. Unfortunately,
they also need to be one-to-one and this is not the case for
what I do when importing or what Ramana does when importing or
exporting without some assumptions. What assumptions can we
reasonably make?

Regards,

Rob.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20140218/80b3bd92/attachment.html>