[opentheory-users] Type variables

[Rob Arthan]

The OpenTheory "thm" command  allows for an alpha-conversion to get the variable names in a theorem exactly right. The description doesn't say anything about type instantiation, so presumably type variable names have to be right already. Perhaps it should allow type variable renaming too, because the choice of type variable names in definitions of existing constants (like the quantifiers) is going to be implementation-dependent. Unfortunately, this is a little tricky to specify and implement because "thm" also allows the inferred theorem to have fewer assumptions than the target theorem. 

On this topic, the Gilith OpenTheory Repo seems to use HOL Light type variable names (A, B, C etc.) that can't be parsed in HOL4 or ProofPower. In any case, if "thm" doesn't allow for type variable renaming, then the documentation needs to say what type variables have been used.

Regards,

Rob.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20131129/ca689d4e/attachment.html>