의미론적 패키지: \inference가 중첩된 부동 전제

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}