That auto-transformation we mention, is what? Do you mind explaining? On Mon, Dec 2, 2024, 14:45 'Thierry Arnoux' via Metamath < [email protected]> wrote:
> On 02/12/2024 13:29, savask wrote: > > I have a question: do you use some automation (tactics) to do > > substitutions into the identity, like deriving step 23 of your M<P > > file? Or you simply remember the movements by heart? > > Recently I've been using Yamma. Unfortunately it does not have > auto-transformations like MMJ2, so there is no tactics for automatically > proving e.g. variable substitutions. > > Most of the time I work backwards, from the formula I want to prove. > Yamma proposes a reduced list of theorems which could lead to that > result, and I choose from the list, partly from my memory. > > Otherwise I'm either entering the formula and letting the tool find the > correct theorem to apply, or remembering the name of the theorem I want > to apply, and letting the tool build the resulting formula. > > > -- > 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/c8811771-bd98-4d95-96b9-1839a1d73505%40gmx.net > . > -- 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/CAAoC84xxiqcgZz1ywZhiG3sTdnu0QppHyFsn5RHzEjgJ_EfsQw%40mail.gmail.com.
