LaTeX rendering

[mario]

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

[Thierry Arnoux]

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, 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

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/ee2bb0f9-d530-45d2-8f35-e1d026e67fafn%40googlegroups.com.

[mario]

I have been able to install MMJ2.

Thanks Best wishes

m.