Thanks! Yes I also just discovered the MMT functionality, so I can set a folder and I don't need to edit anything manually.
The menu "TL"->"Unify+Store in MMT folder" apparently emits a directly suitable MMT file, which I just append with "cat myMMT/theproof.mmt >> Sandbox.mm" Sandbox.mm was initially just an empty file with "$[ Sandbox.mm $]" It took me a while to figure out... Thanks for your help! Ludwig Op woensdag 19 april 2023 om 15:13:40 UTC+2 schreef Peter Mazsa: > On Wed, Apr 19, 2023 at 1:49 PM LM <[email protected]> wrote: > > I am confused how to export proofs so I can include them in my > sandbox.mm file (which includes $[ set.mm $] ) > > mmj2 loads your set.mm file: try to edit you local set.mm. When you > are ready with a proof in mmj2, you should format it similarly to what > you see in set.mm. > For example, this proof in mmj2 > $( <MM> <PROOF_ASST> THEOREM=dfcnvasymrel4 LOC_AFTER=? > * Alternate definition of the converse asymmetric relation predicate. > (Contributed by Peter Mazsa, 25-Mar-2023.) > 50::dfcnvasymrel2 |- ( CnvASymRel R <-> ( ( ( _V X. _V ) \ R ) C_ `' > R /\ Rel R ) ) > 51::relcnv |- Rel `' R > 52::relvvdifss |- ( ( Rel R /\ Rel `' R ) -> ( ( ( _V X. _V ) \ > R ) C_ `' R <-> ( R u. `' R ) = ( _V X. _V ) ) ) > 53:51,52:mpan2 |- ( Rel R -> ( ( ( _V X. _V ) \ R ) C_ `' R <-> > ( R u. `' R ) = ( _V X. _V ) ) ) > 54:53:pm5.32ri |- ( ( ( ( _V X. _V ) \ R ) C_ `' R /\ Rel R ) > <-> ( ( R u. `' R ) = ( _V X. _V ) /\ Rel R ) ) > qed:50,54:bitri |- ( CnvASymRel R <-> ( ( R u. `' R ) = ( _V X. > _V ) /\ Rel R ) ) > $= ( wcnvasymrel cvv cxp cdif ccnv wss wrel wa wceq dfcnvasymrel2 wb > cun relcnv relvvdifss mpan2 pm5.32ri bitri ) ABCCDZAEAFZGZAHZIATM > SJZUBIAKUBUAUCUBTHUAUCLANATOPQR $. > $) > should be > $( Alternate definition of the converse asymmetric relation predicate. > (Contributed by Peter Mazsa, 25-Mar-2023.) $) > dfcnvasymrel4 $p |- ( CnvASymRel R <-> ( ( R u. `' R ) = ( _V X. _V > ) /\ Rel R ) ) $= > ( wcnvasymrel cvv cxp cdif ccnv wss wrel wa wceq dfcnvasymrel2 wb > cun relcnv relvvdifss mpan2 pm5.32ri bitri ) ABCCDZAEAFZGZAHZIATMSJ > ZUBIAKUBUAUCUBTHUAUCLANATOPQR $. > at the end of your local set.mm . > This must solve some of your problems. > > P. > -- 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/3216ee3a-2d97-46b5-b9c6-8b366dbb333cn%40googlegroups.com.
