семантический пакет: Плавающие помещения с вложенным \выводом

Question

Я печатаю, устанавливая семантику большого шага, используя пакет semanticи его команду \inference.

Я использую компилятор LuaLaTeX.

Однако, когда я составляю больше inferenceкоманд, и одна из них представляет собой аксиому, т. е. правило без каких-либо предпосылок, другая предпосылка начинает плавать. Похоже, что она пытается сделать какое-то вертикальное выравнивание.

Вот пример:

\inference[\(\mathcal{E'}=\) \textsc{EC-IfF}]
{ 
    % ------- THIS PREMISE FLOATS
    \overset{\mathcal{E'_0}}
    {
             \langle b, σ \rangle \downarrow \texttt{false}
    }
    &
    {
        \inference
        [\textsc{EC-Skip}]
        {}
        {
        \langle \texttt{skip}, σ \rangle \downarrow σ
    }
    }
}
{
            \langle
            \texttt{if } b \texttt{ then } 
            (c_0 ; \texttt{ while } b \texttt{ do } c_0)
            \texttt{ else skip}, σ
            \rangle
    \downarrow
    σ''
}

Answer 1

В примере OP базовая линия сохраняется по всему большому "числителю". Хотя можно утверждать, что это правильный способ сделать это, можно переопределить это значение по умолчанию, \abovebaseline[-\dp\strutbox]{...}применив его к выводу ED-Skip.

\documentclass{article}
\usepackage{semantic,amsmath,stackengine}
\begin{document}
\inference[\(\mathcal{E'}=\) \textsc{EC-IfF}]
{ 
    % ------- THIS PREMISE FLOATS
    \overset{\mathcal{E'_0}}
    {
             \langle b, σ \rangle \downarrow \texttt{false}
    }
    &
    {
        \abovebaseline[-\dp\strutbox]{\inference
        [\textsc{EC-Skip}]
        {}
        {
        \langle \texttt{skip}, σ \rangle \downarrow σ
    }}
    }
}
{
            \langle
            \texttt{if } b \texttt{ then } 
            (c_0 ; \texttt{ while } b \texttt{ do } c_0)
            \texttt{ else skip}, σ
            \rangle
    \downarrow
    σ''
}
\end{document}