Correction, the Sandbox.mm includes set.mm: ... Sandbox.mm was initially just an empty file with "$[ set.mm $]" ...
Op woensdag 19 april 2023 om 16:22:24 UTC+2 schreef LM: > 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/9538803d-2cb6-4b32-a6ab-72b44ef94922n%40googlegroups.com.
