I would welcome such a convention. Some syntax statements are not associated with definitions (e.g. wi, wn, cv, wal) and I see that you took this into account in your proposal. What would the precise convention be? Is it:
Every statement with label df-xxx is an $a-statement with typecode |- and is immediately preceded by an $a-statement with typecode wff and label wxxx or with typecode class and label cxxx. 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) Handling of df-clab, df-clel, df-cleq ? These are special cases, df-clel and df-cleq for the necessary early position of the associated syntax statements (for "overloading" purpose), and df-clab for the special form of the definition. In any case, I would still like the labelling consistency, e.g. wceq --> wcleq wcel --> wclel 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/95bd1b89-75e4-406c-8385-d307c8fd0549%40googlegroups.com.
