I suggest just changing your note for now. The suffix usage thing requires a more systematic study (it's about consistency, after all), which is a separate issue.
On Sat, Nov 2, 2019 at 8:43 PM David A. Wheeler <[email protected]> wrote: > > > On Sat, Nov 2, 2019 at 1:09 PM David A. Wheeler <[email protected]> > > wrote: > > > There is no label sumeq2dva ; I presume esumeq12dva was intended > > > (if not, please let me know). > > On Sat, 2 Nov 2019 20:35:48 -0400, Mario Carneiro <[email protected]> > wrote: > > Looks like it is sumeq2dv; I guess our usage of the "a" suffix in these > > circumstances is inconsistent (compare mpteq2dv / mpteq2dva vs sumeq2sdv > / > > sumeq2dv). > > I'm happy to fix it, but should we rename sumeq2dv to sumeqdva first, > and then change the text to match? Or should we just use sumeqdv ? > > --- 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/E1iR3yx-0004yh-UC%40rmmprod07.runbox > . > -- 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/CAFXXJSuo%2B5o3rdoMmV%2BcQZXhrSMOhzjM9_yDYPmN2CmUpHJoEA%40mail.gmail.com.
