セマンティック パッケージ: ネストされた \inference による浮動前提

Question

パッケージsemanticとそのコマンドを使用して、いくつかの大きなステップのセマンティクスを設定することを入力しています\inference。

私はLuaLaTeXコンパイラを使用します。

しかし、さらにコマンドを作成しinference、そのうちの 1 つが公理、つまり前提のないルールを表す場合、もう 1 つの前提が浮いてしまいます。垂直方向の配置を試みているように見えます。

次に例を示します。

\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}