I am confused how to export proofs so I can include them in my sandbox.mm file (which includes $[ set.mm $] )
My RunParams load syllogism on startup, which is trivially proven by CTRL + U nification After unification, trying to export it, it errors on the first non hypothesis statement. Is there some guide or tutorial on exporting proofs to .mm format? What does GMMF stand for? Did I forget to install something? Greetings, Ludwig -- 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/874d79c1-a987-4d9d-9828-3c99b0799eefn%40googlegroups.com.
