[opentheory-users] subst

[Ramana Kumar]

Yes I think you're right.

My implementation of tyvar_to_ot would suggest so too.
https://github.com/mn200/HOL/blob/master/src/opentheory/OpenTheoryCommon.sml#L9


On Mon, Aug 12, 2013 at 12:00 PM, Rob Arthan <rda at lemma-one.com> wrote:

> In the description of subst in the article file format, the a_i are type
> variable names, so presumably they must be in the global namespace?
>
> Regards,
>
> Rob.
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20130812/a679e5f2/attachment.html>