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

[Rob Arthan]

I withdraw comment (7). I must have had a mental aberration reading the description of the command that pushes an integer

On 2 Aug 2013, at 15:21, Rob Arthan <rda at lemma-one.com> wrote:

> ... and one more for luck:
> 
> 7) the examples of the int primitive type include -5, but it actually not possible to get a negative number onto the stack, I believe.
> 
> On 2 Aug 2013, at 15:15, Rob Arthan wrote:
> 
>> Dear All,
>> 
>> I have a few (mainly editorial) comments on the article file format definition (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.)
>> 
>> 2) In the description of the virtual machine, it would be helpful to say that some commands impose constraints on the states in which they can be executed (e.g., free variable conditions or constraints on types). Presumably it is left to the implementor to decide what to do if errors occur.
>> 
>> 3) With just two exceptions (as far as I can see), the "notes" in the command description are actually constraints that restrict the states in which the command can be executed. It would be clearer to label them as "constraints" or "restrictions" rather than just "notes". The two exceptions are the note on ref and the second note on varType, which are both just informative.
>> 
>> 4) In appTerm and appThm, the type of f must have the form sigma -> tau where sigma is the type of x.
>> 
>> 5) For ref and remove, k must presumably be in the domain of dict.
>> 
>> 6) The notes on var and varType, both refer to the "global namespace", but this term is not defined. I presume it means a name of the form Name([], s).
>> 
>> 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