I’d like to create derivations trees for a type evaluation (dunno what this is exactly called). Basically I want to reproduce this bottom up „tree“ on page 15 from http://lucacardelli.name/papers/typesystems.pdf.
The closest thing I’ve found yet is posted in the comment (LaTeX for logicians) since I have <10 reputation an can only post one link. But there may be a package for exactly this or an easy way for doing this.
I already build single parts of the tree with
% 1: numerator
% 2: denominator
% 3: rule name
% 4: label without eqn:, can be referenced with \eqref{eqn:#4}
\newcommand{\ruledef}[4]
{
\begin{equation}
\fontsize{11pt}{12pt}\selectfont
\tag{\textsc{#3}}
\frac{\text{#1}}{\text{#2}}
\label{eqn:#4}
\end{equation}
}
This creates a single part of the tree with the tagon the right side. But I don‘t know how to have two of this equations on the same height with their tag right near them. Also I don’t know to center these equations and bundle them alltogether.
proof
topic on CTAN.