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

[Joe Leslie-Hurd]

Hi Rob,

Thank you very much for your comments on the article standard. I've
incorporated all of them (except the one that you withdrew) and it is
much clearer now. Since these were minor edits, I don't intend to bump
the version, so it's still article format version 5.

> 1) I think it would be helpful to say in the description of the primitive
> types that the primitive type const stands for the name of the constant only
> whereas var stands for a variable name together with a type (I am intrigued
> by this design decision, but don't have any technical objection to it.)

The rationale underlying this design is that I wanted defineConst to
return a constant together with its definition theorem

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

that could be used to construct terms, and the simplest way to do this
was for constants to contain only their name and allow the user to
attach different types to them when constructing terms. (I did
consider an alternative design where constants contained their
principal type, but there was an extra substitution command that
operated on terms, but that seemed more complicated.)

On the other hand two variables with the same name and different types
are treated as completely different variables, so it made sense for
variables to contain both their name and type.

Thanks again for the feedback,

Joe