I use minimize_with * quite routinely (like, every time I prove something, usually). I haven't timed it with and without the discouraged tag on 4syl but that would be my benchmark.
This command is already pretty slow much of the time. On June 14, 2019 7:06:03 AM PDT, 'Alexander van der Vekens' via Metamath <[email protected]> wrote: >Why is the theorem ~ 4syl discouraged? The comment says: > >The use of this theorem is marked "discouraged" because it can cause >the >> "minimize" command to have very long run times. However, feel free >to use >> "minimize 4syl /override" if you wish. Remember to update the Travis > >> "discouraged" file if it gets used. >> > >Actually, there are 191 uses of "4syl" in set.mm! So is there (still) >a >relevant impact on "minimize" or another reason why it is discouraged? > >In my opinion this theorem is quite useful and therefore should be >usable >again (tag "(New usage is discouraged.)" should be removed). > >-- >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/772685bd-4c6b-41a1-b907-789fe6fbea26%40googlegroups.com. -- 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/6DF9952D-8904-4B5D-95AB-04B0D3C9D2F8%40panix.com.
