[opentheory-users] Troubleshooting an article reader

[Joe Leslie-Hurd]

Hi Mario,

> One thing that is not well explained in the spec is the definition of
> alpha-equivalent, even though it is used several times.

Thanks for the feedback. I've added Ramana's one-sentence description
of alpha-equivalence (with an example and a non-example) to the
description of the term type near the top of

http://www.gilith.com/research/opentheory/article.html

I also added an example of distinct variables with the same name,
following our discussion yesterday.

>> I intend to write a translator from OpenTheory to Metamath
>> [http://us.metamath.org/index.html].

That sounds really interesting, especially the difference in the
substitution primitives. I look forward to hearing more about it.

Cheers,

Joe