On Saturday, September 5, 2020 at 2:46:44 AM UTC-4 Alexander van der Vekens wrote:
> That's sound really great! I will try this new feature soon, using the > friendship theorem as "root"... > Good choice. I was curious so I added it (temporarily) here: http://us2.metamath.org/ocat/friendship/mmtheorems.html Who would have known that it depends on Stoic logic? :) I wrote about something similar that included the /extract functionality (but with a much more ambitious goal in mind) in 2014: https://groups.google.com/g/metamath/c/hrtD9_wAcHM/m/fHL85-Hx5usJ set.mm was put on GitHub about 6 months later, addressing some of the issues I brought up, and the idea of extract/merge was put on hold. But I've always felt /extract could provide insight about a particular theorem, and if nothing else would give you an idea of what background you need to understand it fully. 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/718e5102-91c9-4215-94c0-50fb53387b70n%40googlegroups.com.
