mathpartir：ottalt 将 mathpartir 前提分别放在各自的行上

Question

我正在使用 Ott 工具为编程语言论文中的一些推理规则生成 LaTeX。为了使输出看起来不错，我使用了奥特·阿尔特图书馆。

OttAlt 基于 mathpartir，它的一个主要特性是它可以在前提之间自动添加换行符，这样短的前提都在同一行，而长的前提会被分开。

问题是，当我使用 OttAlt 时，它似乎总是将每个前提放在其自己的行上，即使我选择了该implicitPremiseBreaks选项。

问题似乎出在前提和ottdefnblock宏重新定义。

有谁知道为什么 ottAlt 会破坏场所的自动间距？

我真的不想手动插入所有的换行符，但我还想通过将小处放在一行上来节省空间。

这是 MWE。它依赖于非 CTAN 包，所以我无法拥有自托管的 MWE，但这里是主文件：

%% Generated from the following Ott file:


% metavar exprvar, x, y, f ::= 
%    {{ coq nat }} {{ coq-equality }} 
%   {{ tex \mathit{[[exprvar]]} }} {{ com  term variable  }} {{ lex alphanum }} {{ texvar \mathtt{[[exprvar]]} }}


% grammar


% e,t  :: tm_ ::= {{ com terms }}
%   | x            ::   :: var  {{ com variable }}


% G  :: env_ ::= {{ com typing contexts }}
%   | empty        ::   :: nil  {{ com empty }}

% defns Jtype :: '' ::=

% defn G |- e : t :: :: typing :: T_ {{ com term typing }} by


% G |- x : t
% G |- x : t
% G |- x : t
% G |- x1111111111111111111111111111111111111111111111111111111111 : t
% ---------- :: Var
% G |- x : t



\documentclass{article}

\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{mathpartir}



\usepackage[implicitPremiseBreaks]{ottalt}


\inputott{ott_out}

% \renewcommand{\ottpremise}[1]{#1}


\begin{document}

OttAlt:

%Doesn't work, puts each on its own line
\ottdefntyping{foo}

MathPartir:

\begin{mathpar}
\inferrule{G |-x : t \\ G |-x : t \\ G |-x : t \\ G |-x_{1111111111111111111111111111111111111111111111111111111111111111111} : t }{Foo}
\end{mathpar}

\end{document}

\end{document}

输出：