Hello! > The metamath-knife utility has the -F option to output Metamath's database formulas as s-expressions since version 0.3.9 <https://github.com/metamath/metamath-knife/releases/tag/v0.3.9> , which is a prefix format with parentheses.
Yes that's what I needed, thank you Thierry! > Metamath-knife also has the option -e to output the full proof of a single statement in MMP format (with steps in ASCII, not as S-expressions), as a file. Even better! Thanks, and to you Glauco too! Now it seems theorem auto-proving is blocked on my efforts only :-) Best regards, Ender пятница, 28 марта 2025 г. в 18:52:07 UTC+3, Glauco: > Thanks for the clarification, Ender > > I thought you were referencing the proof format, but you were clearly > addressing the statements. > > Appreciate your patience! > > 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 visit https://groups.google.com/d/msgid/metamath/cefcc197-cd7c-4c4f-9f6e-4871b4ab4312n%40googlegroups.com.
