[opentheory-users] subst

[Joe Leslie-Hurd]

Hi Rob,

Yes, that is indeed a constraint of the subst rule, and I've added it
to the description.

Thanks for your suggestions, I want to make the standard as clear as possible.

Cheers,

Joe

On Mon, Aug 12, 2013 at 9:26 AM, Ramana Kumar <ramana at member.fsf.org> wrote:
> 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
>>
>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>