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/4f37276f-f8d1-8d5f-86a0-4f9e9981479d%40gmx.net.
