[opentheory-users] type variable names

Ramana Kumar ramana.kumar at gmail.com
Sun Sep 4 14:55:49 UTC 2011

Unfortunately, type variables cannot be bound, so their names matter.
Is the convention for their names in OpenTheory specified somewhere?
Looking at the base package, for example, one might guess that type
variables are named by uppercase letters starting from "A".
If this convention ought to be relied on, then it would make sense for
article readers and writers for HOL4, for example, which has a
different convention, to translate between "A" and "'a" automatically
(just as they should translate term constants, e.g. between
"Data.Bool.select" and "min$@").
Am I right?

More information about the opentheory-users mailing list