On Sun, 15 Dec 2019 13:02:33 -0800 (PST), Benoit <[email protected]> wrote: > Like FL, I think several lemmas deserve to be in the main part.
I believe that all "Metamath 100" results (and thus all they depend on) should eventually move into the main body. After all, all Metamath 100 results are results that at least some others believe are important. We don't have to do that *instantly* of course. In many cases I expect there will be discussion as the dependencies are examined, possibly generalized, and then moved into the main body in groups over time. I think it's important to keep working on getting more things moved from mathboxes into the main body. Tools like mmj2 only consider items in the main body for many automated steps, and in any case I think it's far more sensible to readers if major results are properly organized in the main body. --- 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/E1igeJf-00078p-EP%40rmmprod07.runbox.
