How-Tos and best practices

[Alexander van der Vekens]

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?

I think everybody adding new theorems to set.mm and proving them (or shortening already existing proofs) has a lot of experience which can be useful for others.

Therefore, I would propose to create a "page" where How-Tos and best practices for writing theorems and proofs for set.mm can be documented. I do not know if the Wiki on Github would be the best place, or should it be a *.raw.html page?

A starting point for such a page could be the two "tasks" mentioned above...

Best regards,

Alexander

[Mario Carneiro]

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

Mario

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/2870738f-a2af-40b2-a31b-b9aa4f8cd000n%40googlegroups.com.

[Benoit]

On Monday, April 19, 2021 at 12:52:06 AM UTC+2 di....@gmail.com wrote:

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

Mario

I agree.  Also, this would give an opportunity to organize the metamath/set.mm github repository (see https://github.com/metamath/set.mm/issues/1887).

Benoît

[ookami]

Perhaps one should extend http://us2.metamath.org:88/mpeuni/conventions.html properly.

Wolf

[David A. Wheeler]

On Sun, Apr 18, 2021 at 9:48 AM 'Alexander van der Vekens' via Metamath <meta...@googlegroups.com> 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 <meta...@googlegroups.com> 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