On Monday, January 6, 2020 at 1:03:23 AM UTC-5, Mario Carneiro wrote: ... > > I wish we would stop using the description comment for metadata like this. > This is the sort of thing that makes markup parsing the rats' nest that it > is. Just have a separate comment, with a sane computer-readable grammar. > (It should also contain the "contributed by" and "usage discouraged" > information, which are also metadata. Using english words just fools people > into thinking there is no strict grammar.) >
I understand your point and agree that is it something we need to revisit longer term. However, practically speaking, the "(New usage is discouraged.)" and "(Proof modification is discouraged.)" tags are very clear in English to the user and have been quite successful in accomplishing their purpose, especially given that not all tools recognize them or implement them fully. They are included in the main description so the user will see them and treat the axiom/theorem accordingly. I think we would want to make sure all major assistants and IDEs adequately support these before hiding them in a $j comment. As for the acknowledgments, shouldn't they really be part of the description as opposed to a $j directive? Their purpose is just to inform the reader. 'verify markup' does some cursory checking for consistency, but they don't impact the way the theorem is treated by a proof assistant. Recall that a few years ago we went the other way, moving the separate proof date stamp into the main comment. Norm -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/1ad38f86-8183-4872-a53d-dcd3f17fe684%40googlegroups.com.
