I completely missed the wiki page and CONTRIBUTING.md file (probably because I couldn't see them in http://us2.metamath.org:88/mpeuni/mmset.html ). They both answer many questions I thought were not covered anywhere, so I guess they serve as a guide.
I would still like a tutorial with examples, but I don't dare making one, since I'm not a regular contributor. In any case, some contributing technicalities most probably won't stop a person who already managed to prove something in metamath, and materials you linked answer most questions anyway. -- 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/ed8b8df5-4082-4ae8-a756-e7fac0534b81%40googlegroups.com.
