My workaround with mmj2 was (given ~ example to be changed): - create a ~ exampleNEW (with the new signature) - search all proofs using ~ example - load each in mmj2 and change it to use ~ exampleNEW (then create the .mmt files) - remove ~ example from the theory and reload the theory - copy ~ exampleNEW and rename it to ~ example - load in mmj2 each proof using ~ exampleNEW and change it to use the new ~ example - remove ~ exampleNEW
I'd like to know if there is a better workflow in mmj2 Il giorno domenica 26 novembre 2023 alle 17:40:00 UTC+1 [email protected] ha scritto: I have my workarounds to handle these kinds of changes using mmj2 but having the tool understand it better sounds like it could be a significant help. -- 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/04f8c8c5-206f-4944-8cad-fedc8a80ea0cn%40googlegroups.com.
