> 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.
