On Mon, 6 Jan 2020 01:03:10 -0500, Mario Carneiro <[email protected]> wrote: > My understanding of Norm's proposal is that this is a markup feature only. > People won't actually look at 3:2+eq+tr+4:3+d -- it's no better than the > original in terms of human readability -- but the index of "meanings" of > 3:2 and eq and so on can be stored in a separate file so that it can parse > 3:2+eq+tr+4:3+d and turn it into an interactive display...
I think "eq+tr" *is* better for human readability than "eqtr", because then the human *knows* that it's a combination of "eq" followed by "tr" (instead of, say, some "eqt" followed by an "r"). So while it's okay for the label to be unchanged, it *is* useful to have this information near the assertion itself. The problem for human readability is the proposed colon notation. If you're going to use colons, it might be better to have a textual gloss like "3:triple" instead of "3:2". Then I know which 3 is meant. > I wish we would stop using the description comment for metadata like this. I think putting the information in a *separate* file would be a mistake. In my experience, every time you have separate datasets with the same key (e.g., a label), you're creating a slow-running disaster. The datasets will quickly go out of sync, and it will become difficult to *keep* in sync. In contrast, if the information goes into the description, then keeping things in sync is quite trivial, and errors become both obvious and easy to correct later. In addition, if the information is right there, it's easily accessible to later users and readers; if it's in a separate file, it will often not be seen. We could formalize the grammar of the description field & perhaps add some tweaks to make it easier to parse in detail. I think that would be a better direction than having a separate file that goes quickly out-of-sync and is rarely viewed. We want things to be *easy* to maintain (correctly) over time, after all. --- David A. Wheeler -- 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/E1ioVmp-0000ZZ-11%40rmmprod07.runbox.
