On Monday, January 6, 2020 at 7:03:23 AM UTC+1, 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 think this would go in the good direction. I can make a loose analogy with another math hobby I contributed to: Neil Sloane's Online Encyclopedia of Integer Sequences (OEIS). Every set.mm proof has its own webpage (in the Metamath Proof Explorer), which in some respects has similarities with each sequence of the OEIS and its webpage (e.g., each has a name/label, a comment, an author, a date, etc.). The format is explained at http://oeis.org/eishelp2.html with a link to the description of the "internal format" (for an example, see e.g. http://oeis.org/A3). Benoît -- 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/00306608-3dc2-4150-a90f-5825655035a3%40googlegroups.com.
