Not that I'm discouraging you from making this better in Yamma but what I do in mmj2 is:
1. Load the file in mmj2 and save .mmp files for everything I want to work on. Quit mmj2. 2. Go to a text editor and make changes to hypotheses or whatever it is. 3. Load the .mmp files. Steps that don't work any more will show an error but you can use mmj2 to help fix those errors (there's a bit of an art to that given how mmj2 handles different kinds of errors but I won't attempt to describe that in full detail here). What you describe for mmj2 also works, I'm pretty sure I sometimes do that too (for some changes having the old and new both around at the same time can be helpful). On November 26, 2023 12:33:26 PM PST, Glauco <[email protected]> wrote: >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. -- 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/898AE29A-D5B4-4CA2-A6D6-B4FD95FEFCF9%40panix.com.
