On Mon, Jan 6, 2020 at 12:03 PM David A. Wheeler <[email protected]> wrote:
> 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. > Humans are generally good at segmentation, and I don't think that the lack of segment markers in labels has been a significant problem historically (and there is some evidence in this thread that putting segment markers in would make readability worse). We can play with alternative displays on the web page and so on, but I would like to keep set.mm (labels and proofs) as they are currently. 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. > The point here is to centralize and enumerate all glosses for the meanings of label segments. Assuming that a program is used for transforming this data into something human readable, it doesn't bother me how it gets stored. But if we have longer glosses then these too need to be defined and possibly kept to a reasonable size. > > 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. > I didn't say it should go in a separate *file*, I said a separate comment. We used to have dates in separate comments, after the proof. We could do a similar thing with metadata, either before or after the theorem. Label glosses are not directly related to theorems (because there is a many-to-many relationship between label segments and theorem labels), so it makes sense to have those stored separately. Mario -- 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/CAFXXJStvUM2ohUSBBx4xYfX5THEJX-DzWrm7OuB4_ZpY2xQ88g%40mail.gmail.com.
