Hi Matthew, do you have a specific partial .mmp file where you would expect unification to fail or take forever so that I can test it with Yamma? (so far I've not been able to find one; with every new major update I try unification in the proof of ~ fouriersw that's more than 1500 steps and contains some steps with "many" hyps)
I've loaded the proof of ~ segconeq that contains two steps justified by ~ syl333anc . If I remove the labels and the refs from both steps, Yamma finds them with no lag. Maybe I've not understood the example you were referring to? Thanks in advance Glauco p.s. before trying what I call "step derivation" (not sure if mmj2 uses the same nomenclature), all parsing nodes for all theorems in set.mm need to be computed and in my slow VM it takes about one minute (it is done by a separate working thread in the background) -- 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 visit https://groups.google.com/d/msgid/metamath/61681cd8-f663-4bd3-b650-06d076be97b1n%40googlegroups.com.
