On Saturday, June 15, 2019 at 4:42:22 PM UTC+2, David A. Wheeler wrote: > > On Sat, 15 Jun 2019 07:05:43 -0400, Mario Carneiro <[email protected] > <javascript:>> wrote: > > I would like to get away from label conventions in favor of something > > machine readable and not hardcoded. > > I'm fine with adding additional mechanisms. > However, I'd like to keep using & enforcing the label conventions. > I find they're very helpful for the humans who are trying to read this > stuff :-). > And once the humans start depending on the conventions, it's wise > to enforce the conventions so the fragile humans aren't misled. > > Label conventions are also "machine readable". You can make them > not hardcoded by adding a mechanism to declare the label convention.
I also think that sticking as close as reasonably possible to label conventions makes it easier to humans (and this contributes to making metamath more attractive). > The mechanism I propose is: > > > > If an $a statement is given for a syntax typecode (i.e. not |-), then > it > > is a definition iff the immediately following statement is a > definitional > > axiom $a |- foo = ... which satisfies the usual rules. Otherwise, it is > > treated as an axiom, and a warning is issued if the label convention > > implies that the axiom would like to be treated as a definition and > there > > is no warning-suppressing pragma attached to the axiom. > > That's extremely strict. Even though we don't use it in set.mm today, > I worry about being unable to escape it later. > I'd prefer that to be the *normal* case, but with a special statement > (say a $j) that means "it's a definition even though it's down here" > statement. > Indeed, I think that one should allow exceptions documented with a $j statement. I ran into a concrete example recently: I want to eventually define multiplication of extended complex numbers (~df-bj-mulc) from the beginning, but in the infinite case, it requires ~clog (through complex argument), which has to be defined much later. But this does not prevent one to use multiplication in the finite case meanwhile. Therefore, the whole thing would look like: clog $a class cmulc $a class df-mulc $a |- [many theorems] df-log $a |- There are probably several cases already in set.mm (although they should be kept exceptional). > > Some label changes I see (skimming through mmdefinitions.html) are: > > > wb --> wbi (and similarly for wo wa, w3o, w3a, wxo), even though > df-bi > > > is a special case > > > df-v --> df-vv (to match cvv and avoid collision with cv) > > > > The general rule has been to make constant names as short as possible > [...] > > I think conventions are good, even if it would increase the size of set.mm. > > > So I would support switching to "wDFNAME" everywhere. We've already been > moving to increasingly keep our label names consistent with the "df-NAME" > definitions. And while the constant names aren't usually > visible to the user, in your lean translation they *ARE* directly visible, > and they're also visible in the HTML showing definitions. > I also think that having the label df-xxx correspond to wxxx or cxxx is a good convention to stick to. As David says, the compressed size of set.mm would not increase. Side question: would you extend this rule to the $c-statements? i.e. have blocks $c smurf $. csmurf $a class smurf $. df-smurf $a smurf = ... $. This would look more systematic. As suggested above, maybe one could also standardize the comments, for example "Extend class notation to smurf / Syntax for smurf / Define smurf, the function that..." ? Benoit -- 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/feb42d0c-a59c-4914-965f-5bc68a776c94%40googlegroups.com.
