On Friday, January 24, 2020 at 11:50:54 AM UTC-5, David Starner wrote: > > When digging through the website theorem list, there's a number of > times one comes upon one or more proofs just used that are just there > to be lemmas for other proofs and have cryptic names. Wouldn't it be > better if those weren't listed on the main theorem list?
The theorem list is created by 'write theorem_list', and by default that command does hide lemmas i.e. statements whose comment begins "Lemma for...". I did it that way for reasons you mention, feeling that they cluttered up the theorem list which was supposed to be a summary. (Another reason was that some lemmas are huge and caused the mpegif version to load painfully slowly in older browsers and computers.) A link to the lemma along with its description is still provided, but it takes up much less space on the web page. However, there were complaints about this because people wanted to see the math content of lemmas on the theorem list page. So I added the qualifier '/show_lemmas' which is now used for the web site generation. What I would suggest is that you download set.mm and metamath.exe (and optionally save the mmset.html web page into the directory to avoid bibliography warnings), then in metamath.exe type 'read set.mm' followed by 'write theorem_list /alt_html' to generate the theorem list locally with the math content of lemmas suppressed. > They'd still > be listed from the proof that uses them. (And if they're used from > multiple proofs, that should be a sign they need a better description > than just "Lemma for x".) > If a lemma is used for multiple proofs, it could be described as "Lemma for abc and xyz...", or perhaps it should just be a regular theorem. Ultimately it is up to the original contributor to put meaningful commentary in the description. But we do try to make incremental improvements over time and welcome suggestions for specific cases. Norm -- 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/f373eece-4743-4882-8310-2f233c0d45be%40googlegroups.com.
