Thanks for the feedback. It works ! :) I see that I should also output the statement and hypotheses along with the proof, so that it could be properly copy-pasted/proofChecked I should also put in there an option, to either output lemmas or to inline them in a big proof
I'll now shut up, work some more and only report when I have got more interesting proofs converted Le vendredi 9 août 2019 23:03:14 UTC+2, Jim Kingdon a écrit : > > Here's what I did. I put the following in set.mm (right before > "Appendix: Typesetting definitions" although the exact location doesn't > matter much. > > mephistolus1 $p |- ( ( 1 + 1 ) + 1 ) = 3 $= > c1 c1 caddc co c1 caddc co c2 c1 caddc co c3 c1 c1 caddc co c2 c1 > caddc > 1p1e2apr1 oveq1i 2p1e3 eqtri $. > > and then I ran metamath.exe and gave it the following commands: > > read set.mm > > verify proof mephistolus1 > > whereupon it printed "mephistolus1" which means it verified (an error > would have printed an error message). > > Exciting to see Mephistolus generating valid proofs! > > On 8/9/19 1:43 PM, Olivier Binda wrote: > > Could someone proofcheck it with another metamath proofchecker > -- 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/b1b9ba37-29ce-440e-a819-e2ee62c89899%40googlegroups.com.
