A few months ago I opened this Rumm issue <https://github.com/tirix/rumm/issues/13>. It involves a bug that, if solved, would allow me to get around the lack of work variables. Perhaps that's a simpler solution?
It wouldn't be as good as having work variables, but it would be better than nothing. At least, I would have a hack to finally support the kind of tactics that are currently impossible to implement without them. -- 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/d62f8d4c-3911-493d-9b26-bfb34c79588dn%40googlegroups.com.
