Norman Megill: > > Typically the conclusion is the part the user is most interested in. So a > > possible rough guideline is to have the label provide a hint about the > > conclusion and not (or rarely) say anything about the > > hypotheses/antecedents. > >
On Mon, 6 Jan 2020 23:39:09 -0800 (PST), "'Alexander van der Vekens' via Metamath" <[email protected]> wrote: > That's a very good and reasonable guideline! Can it be officially > documented somewhere? (and) > > We also don't always need to fully describe the conclusion. For example, > > "cos0" indicates the theorem provides the value for the cosine of 0, but we > > need to look at the theorem itself to see what that value is. "cos0" is a > > nice, concise label I would prefer over "cos0eq1". I agree with both. I've just created a pull request that tries to document both points. See: https://github.com/metamath/set.mm/pull/1390 I expect conversations about naming conventions to occasionally arise. set.mm (and iset.mm!) are becoming larger & larger, which is a good thing, and that increase in scale is making it ever more important to have clear names. --- 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/E1ior6H-00008A-9o%40rmmprod07.runbox.
