Il giorno lunedì 13 gennaio 2020 11:51:18 UTC+1, Alexander van der Vekens ha scritto: > > > Looking for idi in the current version of set.mm, there are a lot of > "idi"s in the proofs of the theorems Glauco provided in December (in his > mathbox)! Since they are very long, I fear that 'minimize' will take a long > time to run. I tried it with a smaller one (~fourierdlem12): 'minimize' ran > some minutes, and decreased the proof from 4678 to 4474 bytes, 11567 to > 10757 steps (567 to 520 essential steps). "idi" was removed by this > minimization, so everything is fine. > > I use idi as a useful tool when writing a proof. It allows to create a "smart" copy of an already proven statement, that may be several lines above the current line.
Using idi I create (just above the current line) a copy of the far away statement (let's say you need to look at it carefully, or you need to copy paste pieces of that statement). A copy paste with a comment could be used, but idi has a number of advantages (the most important, mmj2 automatically updates its step reference if you renumber all the proof). I should never reference those idi steps, I should always reference the step number of the "original" (far away) statement, but sometimes the autocomplete grabs the idi step, instead of the original one. When the proof is done, the plan is to search for any accidental actual use of the idi steps and remove them from the proof (I guess sometimes one slips under the radar...) Glauco -- 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/65625c9e-754b-4cd4-b4af-97ebbd0fbd86%40googlegroups.com.
