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

Joe Leslie-Hurd joe at gilith.com
Mon Aug 5 21:14:46 UTC 2013

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.



More information about the opentheory-users mailing list