On Sat, Nov 2, 2019 at 1:09 PM David A. Wheeler <[email protected]> wrote:
> > On Fri, 1 Nov 2019 20:17:56 -0400, Mario Carneiro <[email protected]> > wrote: > > On Fri, Nov 1, 2019 at 5:00 PM Norman Megill <[email protected]> wrote: > > These are useful tips. I've tried to add a summary of these tips to > mmnatded.raw.html > in this pull request: https://github.com/metamath/set.mm/pull/1236 > > There is no label sumeq2dva ; I presume esumeq12dva was intended > (if not, please let me know). > Looks like it is sumeq2dv; I guess our usage of the "a" suffix in these circumstances is inconsistent (compare mpteq2dv / mpteq2dva vs sumeq2sdv / sumeq2dv). > > --- 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/E1iQwtl-00015C-Ef%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/CAFXXJSspFO%3DwR0xUtFebAJDxiF5tVEp7DaQ-SK_SKiCvcqO-Gw%40mail.gmail.com.
