The Metamath -> MM0 importer already contains a feature for selecting which target theorems you want, so it has the same effect as using /extract on the source database first and then importing it. I've been using numbers for example theorems like dirith or pnt in my talks. I wonder what is the maximum fraction of set.mm you can get by /extracting a single theorem...?
Mario On Sat, Sep 5, 2020 at 5:56 PM Norman Megill <[email protected]> wrote: > 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 > <https://groups.google.com/d/msgid/metamath/718e5102-91c9-4215-94c0-50fb53387b70n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJStNwgd03vBJjUFBZRtuSyrE%3DgsDScRo%2BGhntJ9%3DSL666w%40mail.gmail.com.
