<html><head></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div>I have a problem with edge cases in the mappings of type variable</div><div>names. What currently happens is that I export them as they stand</div><div>and import them by prefixing them with a prime if they don't already</div><div>start with one. Ramana does something more complicated by also </div><div>converting a primed single letter to upper case on output and to</div><div>lower case on input. The upshot of this is 'a in ProofPower imports as 'a</div><div>in HOL4 which then imports back into ProofPower as 'A which imports</div><div>back into HOL4 as 'a and now we are in a loop. This is harmless</div><div>but a bit silly. So should I be adjusting the case like Ramana does?</div><div>And if so why?</div><div><br></div><div>Since a HOL4 or ProofPower theory with non-standard type variable</div><div>names looks a mess and since the Gilith OpenTheory Repo seems</div><div>to have standardised on what HOL4 and ProofPower consider</div><div>non-standard, these mappings are necessary. Unfortunately,</div><div>they also need to be one-to-one and this is not the case for</div><div>what I do when importing or what Ramana does when importing or</div><div>exporting without some assumptions. What assumptions can we</div><div>reasonably make?</div><div><br></div><div>Regards,</div><div><br></div><div>Rob.</div></body></html>