> On Sun, Apr 18, 2021 at 9:48 AM 'Alexander van der Vekens' via Metamath > <[email protected] > <applewebdata://E9D67921-493E-445A-BB7F-2F969B2B0ADA>> wrote: > Recently, there was (again) a discussion how to find theorems whose proofs > can be minimized by a new theorem, and how to change variables of a theorem > (and all proofs depending on this theorem). Norm and Benoît had useful > advices how to do it. I wonder if this should be documented at a central > place. Or is there already something avaiblable? ...
> <Mario> Montag, 19. April 2021 um 00:52:06 UTC+2: > I think such a page would fit best as an additional HTML page on the metamath > web site, which could be developed on github next to the other web pages. (I > don't have any particular suggestions for what to put on the page at the > moment but I'd be happy to review or extend it if someone wants to take a > shot at it.) > On Apr 19, 2021, at 4:16 AM, 'ookami' via Metamath > <[email protected]> wrote: > Perhaps one should extend http://us2.metamath.org:88/mpeuni/conventions.html > properly. I don’t think that’s the right place. The “conventions” page was intended to explain the conventions *within* the final Metamath database file, just like a “conventions” section in a book. However, what’s under discussion is more of a “how to use the tools” and its results would often not be directly visible to readers of a final database. (The reader would just see the minimized proofs, and might have no idea they’re minimized.) Also, there may need to be special formatting to discuss how to use the tools. So I think putting this kind of information in a separate HTML file would make more sense. --- 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/E1028F58-3938-4767-8E6E-C5DC0105F80A%40dwheeler.com.
