I have been able to install MMJ2. Thanks Best wishes m. Il giorno sabato 12 febbraio 2022 alle 16:42:05 UTC+1 Thierry Arnoux ha scritto:
> Hi Mario, > > Welcome to the list! > > The proofs on the Metamath web page are actually displayed in a tree like > way, if you look at the identation: > > Take for example: > > http://us2.metamath.org:88/mpeuni/tfr2.html > > You'll notice the final statement (step 7) has an indentation of "1". The > statements it refers to (steps 5 and 6) both have an indentation of "2", > and so on. It's not strictly a tree, as some tree leafs may be referred to > from different branches (here, step 1 is used both in steps 2 and 6) > > You've already asked about MMJ2, that's the IDE of choice. > > I've built a Metamath plug-in for Eclipse <http://emetamath.tirix.org/>, > but I've also had feedback it's not easy to install. > > I'm sorry I've not used the Latex output, I can't help with that question.. > > BR, > _ > Thierry > > > On 12/02/2022 19:26, mario wrote: > > Hi, > > my first post to this list. > > I am trying Metamath. I have a couple of questions about basic > whereabouts. > > 1. is there a way to customize the .tex file you get with a command like : > *show proof tfr2 /all /lemmon /tex .* > I am getting a .tex file which gives a number of errors when I try to > pdflatex it (mostly missing labels) > > 2. is there a way to output proof in a tree like display (say, sequent > calculi / natural deduction style)? > > 3. is there some kind of IDE for Metamath? > > Sorry if I am asking questions which have been already asked and answered. > Thanks > mario > > > -- > 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/ee2bb0f9-d530-45d2-8f35-e1d026e67fafn%40googlegroups.com > > <https://groups.google.com/d/msgid/metamath/ee2bb0f9-d530-45d2-8f35-e1d026e67fafn%40googlegroups.com?utm_medium=email&utm_source=footer> > . > > -- 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/991f452f-5dd5-45c6-a1a6-45702f3c8d29n%40googlegroups.com.
