[opentheory-users] Some comments on the article file format definition

[Joe Leslie-Hurd]

Hi Rob,

I appreciate the pedantry; thus far too few people have thoroughly
tested the readability of the standard.

> 8) You introduced a typo: "succesful".

Got it.

> 9) It might be clearer to express the constraints on the name in var and varType using pattern matching.

After some thought I decided to make name a primitive type in the
standard and add some explanation of the OpenTheory hierarchical
namespace. Initially I was resisting this, thinking that each theorem
prover developer would prefer to use their native representation of
names. But this just resulted in confusion in the article format, and
in any case developers will need to understand the structure of
OpenTheory names to use the standard theory library.

Cheers,

Joe