On 02/12/2024 17:52, Jorge Agra wrote:
That auto-transformation we mention, is what? Do you mind explaining?
For example MMJ2 is able to automatically expand this proof snippet from just the last step: 9::oveq1 |- ( b = Y -> ( b .o. ( X .o. Y ) ) = ( Y .o. ( X .o. Y ) ) ) 10:9:oveq2d |- ( b = Y -> ( ( X .o. Y ) .o. ( b .o. ( X .o. Y ) ) ) = ( ( X .o. Y ) .o. ( Y .o. ( X .o. Y ) ) ) ) 11::id |- ( b = Y -> b = Y ) !12:10,11:eqeq12d |- ( b = Y -> ( ( ( X .o. Y ) .o. ( b .o. ( X .o. Y ) ) ) = b <-> ( ( X .o. Y ) .o. ( Y .o. ( X .o. Y ) ) ) = Y ) ) All it needs is the exclamation mark before the label and once the Unify command is called (Ctrl-U), it will generate all 3 steps above. Yamma does not have this and I manually fill in `eqeq12d` among a short list. Then it will automatically find `id` as it is a one-step proof. I have to choose `oveq1d` over a short list (the first theorem in the list is often the correct one), and finally it find `oveq1` automatically. MMJ2's auto-transformation is mentioned here: https://github.com/digama0/mmj2/blob/c8dd05548139c7003220caedde65a7abe44a00bf/CHGLOG.TXT#L47 -- 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/4bf02ef4-c032-4acb-9d5b-741dc8600ca6%40gmx.net.
