[opentheory-users] Theorem meta-data

[Mario Carneiro]

I think it will be more backwards-compatible to use a pragma instead, since
this is already used by various interpreters. Regarding the arguments
against pragmas:


> 2. It should be maintained by tools processing articles (when
> possible). Note that pragmas are discarded by the opentheory tool, so
> fail this test for encoding meta-data.
>

This is easily fixed by making the opentheory tool not discard pragmas (or
at least specific pragmas, see below).


> 3. It should be a standard scheme, not reader-dependent, so pragmas
> also fail for this reason.
>

The way to work a pragma into the standard is to reserve certain pragma
names within the standard itself. For example, the current standard
suggests the pragma ["thmName", name] for setting a theorem's name - in a
revision to the standard, just require that this specific pragma be honored
when possible, and leave the rest (any pragma not of this form) to be
user-defined.

For the current purpose, a pragma ["metadata", meta] would satisfy the
desired conditions. The main drawbacks are that it is more verbose and also
does not directly connect itself to the associated theorem, but it gains
the ability to mark other statements, like intermediate theorems.

Mario
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20141107/d1497758/attachment.html>