<div dir="ltr">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:<br><div class="gmail_extra"> <div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
2. It should be maintained by tools processing articles (when<br>
possible). Note that pragmas are discarded by the opentheory tool, so<br>
fail this test for encoding meta-data.<br></blockquote><div><br></div><div>This is easily fixed by making the opentheory tool not discard pragmas (or at least specific pragmas, see below).<br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">

3. It should be a standard scheme, not reader-dependent, so pragmas<br>
also fail for this reason.<br></blockquote><div><br></div><div>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.<br><br></div><div>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.<br><br></div><div>Mario<br>
</div></div></div></div>