0

I'm using a tool to generate large amounts of LaTeX, which contain inference rules that I'm typesetting using mathpartir.

Below, I've got a MWE that's very similar to the code I've got generated. What I'd like to do is redefine it as \renewcommand{\ottpremise}[1]{#1\\}, to separate each of the premises in mathpartir. This allows it to decide where to add linebreaks, which is the main feature I'm going after.

However, when I do this, I get the following error:

Argument of \\ has an extra }.

I think the problem might have something to do with the fact that there's an extra \\ left over after the last premise.

What is causing this error? Is there a way to nicely add \\ between my premises, given that each is wrapped in a call to \ottpremise? Is it necessary/possible to avoid the extra \\ at the end?

Here's the code:

\documentclass{article}

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


\newcommand{\ottdefntstep}[1]{
    \begin{ottdefnblock}[#1]{
    $\Gamma  \mid  \Theta  \vdash  \mathit{T}  \leadsto  \mathit{T'}$
    }{}
\ottusedrule{\ottdruleTStepAssoc{}}
\end{ottdefnblock}
}

\newcommand{\ottdruleTStepAssoc}[1]{\ottdrule[#1]{%
\ottpremise{\Gamma  \mid  \Theta  \Vdash  \tau  :  \mathit{D}  \langle  \tau_{{\mathrm{1}}}  , \, .. \, ,  \tau_{\mathit{n}}  {;}  \mathit{X}  \mapsto  \tau'  \rangle}%
\ottpremise{\Gamma  \mid  \Theta  \vdash  (   [  \tau'  /   \mathit{X} _ \mathit{D}   ]   )  \leadsto  \mathit{T'}}%
}{
\Gamma  \mid  \Theta  \vdash  \mathit{T}  \leadsto  \mathit{T'}}{%
{TStepAssoc}{}%
}}

\newcommand{\ottusedrule}[1]{#1\and}

\newcommand{\ottdrule}[4][]{{\inferrule[#4]{TODO #2 TODO}{#3}}}
\newcommand{\ottpremise}[1]{#1}

\begin{document}

\newenvironment{ottdefnblock}[3][]
{
    \begin{mathpar}
        }
        {
    \end{mathpar}
}

\ottdefntstep{}
\end{document}
  • You can't add the \\ within the \inferrule call? So you'd get {TODO \\ #2 \\ TODO} indeed avoiding an "empty" \\ – remco Apr 6 '18 at 6:17
  • @remco the idea is that #2 is a sequence of premises, and i want all of them separated by // – jmite Apr 6 '18 at 6:22
  • You can't, sorry: mathpartir needst to see \\ in order to separate the premises; if you hide it in a macro, it will not work. – egreg Apr 6 '18 at 7:40
  • Then, if you can only modify the \ottpremise command, I don't think what you want is possible: your \ottpremise code would have to figure out if the current `\ottpremise' is the last in a series. – remco Apr 6 '18 at 7:41
  • @egreg that would explain why a quick test with xparse didn't work... – remco Apr 6 '18 at 7:43

This site is temporarily in read only mode and not accepting new answers.

Browse other questions tagged .