%%
%% This is file `mathpartir.sty',
%% generated with the docstrip utility.
%%
%% The original source files were:
%%
%% mathpartir.dtx  (with options: `package')
%% 
%% This is a generated file.
%% 
%% Copyright (C) 2001, 2002, 2003, 2005, 2015, 2020, 2022
%% by Didier Remy <didier.remy(at)inria(dot)fr>
%% 
%% This file is part of mathpartir.
%% 
%% mathpartir is free software: you can redistribute it and/or modify
%% it under the terms of the GNU General Public License as published by
%% the Free Software Foundation, either version 2 of the License, or
%% (at your option) any later version.
%% 
%% mathpartir is distributed in the hope that it will be useful,
%% but WITHOUT ANY WARRANTY; without even the implied warranty of
%% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
%% GNU General Public License for more details.
%% 
%% You should have received a copy of the GNU General Public License
%% along with mathpartir.  If not, see <http://www.gnu.org/licenses/>.
%%

\NeedsTeXFormat{LaTeX2e}
\ProvidesPackage{mathpartir}
    [2024/01/25 version 1.5.3 Math Paragraph for Typesetting Inference Rules]

%% Identification
%% Preliminary declarations

\RequirePackage {keyval}

%% Options

%% By default, mathpar does not allow page breaks
\newif \ifmathparallowpagebreaks
\mathparallowpagebreaksfalse

\DeclareOption {allowpagebreaks}{\mathparallowpagebreakstrue}

%% Boolean that allows shortdisplays.
%% Not yet activated by defaults
%% The should be no reason not to do so, unless a problem is
%% found with the implementation.
%% This option may/should be removed or inverted in the future. 

\newif \ifshortmathpar \shortmathparfalse
\DeclareOption {shordisplay}{\shortdisplaytrue}

\ProcessOptions

%% More declarations

%% PART I: Typesetting maths in paragraphe mode

%% \newdimen \mpr@tmpdim
%% Dimens are a precious ressource. Uses seems to be local.
\let \mpr@tmpdim \@tempdima

\let \mpr@hva \empty

%% normal paragraph parametters, should rather be taken dynamically
\def \mpr@savepar {%
  \edef \MathparNormalpar
     {\noexpand \lineskiplimit \the\lineskiplimit
      \noexpand \lineskip \the\lineskip}%
  }

\def \mpr@rulelineskip {\lineskiplimit=0.3em\lineskip=0.2em plus 0.1em}
\def \mpr@lesslineskip {\lineskiplimit=0.6em\lineskip=0.5em plus 0.2em}
\def \mpr@lineskip  {\lineskiplimit=1.2em\lineskip=1.2em plus 0.2em}
\let \MathparLineskip \mpr@lineskip
\def \mpr@paroptions {\MathparLineskip}
\let \mpr@prebindings \relax

\newskip \mpr@andskip
\mpr@andskip 2em plus 0.5fil minus 0.5em


\def \mpr@goodbreakand
   {\hskip -\mpr@andskip  \penalty -1000\hskip \mpr@andskip}
\def \mpr@and   {\hskip \mpr@andskip}
\def \mpr@andcr {\penalty 50\mpr@and}
\def \mpr@cr    {\penalty -10000\mpr@and}
\def \mpr@crleft {hskip 4em}
\def \mpr@eqno #1{\mpr@andcr #1\hskip 0em plus -1fil \penalty 10}

\def \mpr@bindings {%
  \let \and \mpr@andcr
  \let \par \mpr@andcr
  \let \\\mpr@cr
  \let \eqno \mpr@eqno
  \let \hva \mpr@hva
  }

\def \MathparBindings {\mpr@bindings}
\def \MathparBeginhook {}
\def \MathparEndhook {}

\def \mpr@assertfalse #1%
  {\PackageError {mathpartir} {\string\inferrule\space #1}{}}%

\let \MathparCentering \centering

%% Old implementation

%% \newenvironment{mathpar}[1][]
%%   {$$
%%      \MathparBeginhook
%%      %% We save \lineskip parameters so that the user can restore them
%%      %% inside math with \MathparNormalpar
%%      \mpr@savepar
%%      %% We define the shape of the paragrah
%%      \parskip 0em \hsize \linewidth \MathparCentering
%%      \vbox \bgroup \mpr@prebindings \mpr@paroptions #1\relax
%%      \MathparBindings
%%      \ifmmode $\else \noindent $\displaystyle\fi
%%      }
%%   {\MathparEndhook \unskip \ifmmode $\fi %$
%%    \egroup $$\ignorespacesafterend}

\newenvironment{mathparpagebreakable}[1][]
  {\begingroup
   \par
   \mpr@savepar \parskip 0em \hsize \linewidth \centering
      \mpr@prebindings \mpr@paroptions #1%
      \vskip \abovedisplayskip \vskip -\lineskip%
     \ifmmode  \else  $\displaystyle\fi
     %$
     \MathparBindings
  }
  {\unskip
   \ifmmode $\fi \par\endgroup %$
   \vskip \belowdisplayskip
   \noindent
  \ignorespacesafterend}

%% The following re-implementation allows for shordisplayskips, 
%% which is used by latex when the last line before the display
%% is much shorter than the white space on the left of the display 

\newdimen \mpr@dim \mpr@dim \z@
\newcount \mpr@count \mpr@count 0
\newif \ifmpr@firstline

\def \mpr@shortabovedisplayskip
   {\abovedisplayskip \abovedisplayshortskip}
\def \mpr@shortbelowdisplayskip
   {\belowdisplayskip \belowdisplayshortskip}

\def \mpr@dim@adjust
   {%% \message {[XXX(3): \the \mpr@dim / \the \mpr@count]}%
    \advance \mpr@dim by -\linewidth
    \mpr@dim -\mpr@dim
    \advance \mpr@count by 2
    %% \message {[XXX(4): \the \mpr@dim / \the \mpr@count]}%
    \divide \mpr@dim by \mpr@count
    %% now \mpr@dim is what is left on each side
    \advance \mpr@dim by -\displayindent
    %% \message {[XXX(5): \the \mpr@dim / \the \predisplaysize]}%
    %% \vadjust {\hbox to \the \predisplaysize {\hrulefill}}%
    }

\def \mpr@cutline 
  {\ifmpr@firstline
      \mpr@firstlinefalse
      \advance \mpr@dim by -\wd0
      \advance \mpr@dim by -\mpr@andskip
      \advance \mpr@count by -1
      \ifdim \mpr@dim > \mpr@andskip
         \mpr@dim@adjust
         \ifdim \mpr@dim > \predisplaysize
            %% \message {[XXX: SHORT \the \mpr@dim / \the\predisplaysize]}%
            \aftergroup \mpr@shortabovedisplayskip
         %% \else
         %%    \message {[XXX: LONG \the \mpr@dim]}%
      \fi\fi
   \fi
   \mpr@dim \wd0
  \mpr@count 0}

\def \mpr@checkdisplay
  {\advance \mpr@dim by \wd0
   \ifdim \mpr@dim > \linewidth
      \mpr@cutline
   \else
      \advance \mpr@dim by \mpr@andskip
      \advance \mpr@count by 1
   \fi}

\def \mpr@short #1%
  {$\egroup
   \mpr@checkdisplay
   \box0 #1%
   \setbox0\hbox \bgroup $\displaystyle}
\def \mpr@shortandcr {\mpr@short{\penalty 50\mpr@and}}
\def \mpr@shortcr
   {\mpr@short{\penalty -10000\mpr@and \mpr@cutline}}
\def \mpr@shorteqno #1{%
   \mpr@short {\penalty 50\mpr@and #1\hskip 0em plus -1fil\penalty 10}}

\def \mpr@shortbindings {%
  \let \and \mpr@shortandcr
  \let \par \mpr@shortandcr
  \let \\\mpr@shortcr
  \let \eqno \mpr@shorteqno
  \let \hva \mpr@hva
  }


\newenvironment{mathpar}[1][]
  {\ifmathparallowpagebreaks
       \mathparpagebrakeable
       \let \endmathpar \endmathparpagebreakable
   \else
    $$
     \MathparBeginhook
     %% We save \lineskip parameters so that the user can restore them
     %% inside math with \MathparNormalpar
     \mpr@savepar
     %% We define the shape of the paragrah
     \parskip 0em \hsize \linewidth \MathparCentering
     \vbox \bgroup \noindent \mpr@prebindings \mpr@paroptions #1\relax
     \ifshortmathpar
         \mpr@shortbindings
         \let \mpr@bindings \mpr@shortbindings
         \MathparBindings
         \mpr@firstlinetrue \mpr@dim \z@ \mpr@count 0
         \noindent \setbox0 \hbox \bgroup $\displaystyle
     \else
         \MathparBindings
         %% should we keep the ifmmode case, which has no counter
         %% part in shortmathpar?
         \ifmmode $\else \noindent $\displaystyle\fi %$
     \fi
     \fi}
  {\MathparEndhook \unskip
   \ifshortmathpar
       $\egroup %$
       \mpr@checkdisplay
       \advance \mpr@dim by -\mpr@andskip
       \advance \mpr@count by -1
       \advance \mpr@dim by \wd0 \box0
       \mpr@dim@adjust
       \ifdim \mpr@dim > \predisplaysize
             \ifmpr@firstline 
               \aftergroup \mpr@shortabovedisplayskip
             \fi
             \aftergroup \mpr@shortbelowdisplayskip
       \fi
   \else
      \ifmmode $\fi
   \fi
   \egroup
   $$\ignorespacesafterend %$
  }

%%% HOV BOXES

\def \mathvbox@ #1{\hbox \bgroup \mpr@normallineskip
  \vbox \bgroup \tabskip 0em \let \\ \cr
  \halign \bgroup \hfil $##$\hfil\cr #1\crcr \egroup \egroup
  \egroup}

\def \mathhvbox@ #1{\setbox0 \hbox {\let \\\qquad $#1$}\ifnum \wd0 < \hsize
      \box0\else \mathvbox {#1}\fi}

%% Part II -- operations on lists

\newtoks \mpr@lista
\newtoks \mpr@listb

\long \def\mpr@cons #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
{#2}\edef #2{\the \mpr@lista \the \mpr@listb}}

\long \def\mpr@snoc #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
{#2}\edef #2{\the \mpr@listb\the\mpr@lista}}

\long \def \mpr@concat#1=#2\mpr@to#3{\mpr@lista \expandafter {#2}\mpr@listb
\expandafter {#3}\edef #1{\the \mpr@listb\the\mpr@lista}}

\def \mpr@head #1\mpr@to #2{\expandafter \mpr@head@ #1\mpr@head@ #1#2}
\long \def \mpr@head@ #1#2\mpr@head@ #3#4{\def #4{#1}\def#3{#2}}

\def \mpr@flatten #1\mpr@to #2{\expandafter \mpr@flatten@ #1\mpr@flatten@ #1#2}
\long \def \mpr@flatten@ \\#1\\#2\mpr@flatten@ #3#4{\def #4{#1}\def #3{\\#2}}

\def \mpr@makelist #1\mpr@to #2{\def \mpr@all {#1}%
   \mpr@lista {\\}\mpr@listb \expandafter {\mpr@all}\edef \mpr@all {\the
   \mpr@lista \the \mpr@listb \the \mpr@lista}\let #2\empty
   \def \mpr@stripof ##1##2\mpr@stripend{\def \mpr@stripped{##2}}\loop
     \mpr@flatten \mpr@all \mpr@to \mpr@one
     \expandafter \mpr@snoc \mpr@one \mpr@to #2\expandafter \mpr@stripof
     \mpr@all \mpr@stripend
     \ifx \mpr@stripped \empty \let \mpr@isempty 0\else \let \mpr@isempty 1\fi
     \ifx 1\mpr@isempty
   \repeat
}

\def \mpr@rev #1\mpr@to #2{\let \mpr@tmp \empty
   \def \\##1{\mpr@cons ##1\mpr@to \mpr@tmp}#1\let #2\mpr@tmp}

%% Part III -- Type inference rules

\newif \ifmpr@premise
\newbox \mpr@hlist
\newbox \mpr@vlist
\newif \ifmpr@center \mpr@centertrue
\def \mpr@vskip {}
\let \mpr@vbox \vbox

\def \mpr@htovlist {%
   \setbox \mpr@hlist
      \hbox {\strut
             \ifmpr@center \hskip -0.5\wd\mpr@hlist\fi
             \unhbox \mpr@hlist}%
   \setbox \mpr@vlist
      \mpr@vbox {\ifmpr@premise
                \box \mpr@hlist
                \ifx \mpr@vskip \empty \else
                  \hrule height 0em depth \mpr@vskip width 0em
                \fi
                \unvbox \mpr@vlist
             \else
                \unvbox \mpr@vlist
                \ifx \mpr@vskip \empty \else
                  \hrule height 0em depth \mpr@vskip width 0em
                \fi
                \box \mpr@hlist
             \fi}%
}

\def \mpr@item #1{$\displaystyle #1$}
\def \mpr@sep{2em}
\def \mpr@blank { }

%% Splits the list of formulas #2 into a stack of lines
%% Mode #1 gives sets mode @premisetrue or @premisefalse
%% for typesetting premises or conclusions

\def \mpr@hovboxT {\mpr@hovbox{\mpr@premisetrue}}
\def \mpr@hovboxB {\mpr@hovbox{\mpr@premisefalse}}

%% @hovbox will be bound to @hovbox@old or @hovbox@new

\def \mpr@hovbox@old #1#2{\hbox
  \bgroup
  #1\relax
  \def \@test {#2}\ifx \@test \mpr@blank\else
  \setbox \mpr@hlist \hbox {}%
  \setbox \mpr@vlist \vbox {}%
  \ifmpr@premise \let \snoc \mpr@cons \else \let \snoc \mpr@snoc \fi
  \let \@hvlist \empty \let \@rev \empty
  \mpr@tmpdim 0em
  \expandafter \mpr@makelist #2\mpr@to \mpr@flat
  \ifmpr@premise \mpr@rev \mpr@flat \mpr@to \@rev \else \let \@rev \mpr@flat \fi
  \def \\##1{%
     \def \@test {##1}\ifx \@test \empty
        \mpr@htovlist
        \mpr@tmpdim 0em %%% last bug fix not extensively checked
     \else
      \setbox0 \hbox{\mpr@item {##1}}\relax
      \advance \mpr@tmpdim by \wd0
      %\mpr@tmpdim 1.02\mpr@tmpdim
      \ifnum \mpr@tmpdim < \hsize
         \ifnum \wd\mpr@hlist > 0
           \ifmpr@premise
             \setbox \mpr@hlist
                \hbox {\unhbox0 \hskip \mpr@sep \unhbox \mpr@hlist}%
           \else
             \setbox \mpr@hlist
                \hbox {\unhbox \mpr@hlist  \hskip \mpr@sep \unhbox0}%
           \fi
         \else
         \setbox \mpr@hlist \hbox {\unhbox0}%
         \fi
      \else
         \ifnum \wd \mpr@hlist > 0
            \mpr@htovlist
            \mpr@tmpdim \wd0
         \fi
         \setbox \mpr@hlist \hbox {\unhbox0}%
      \fi
      \advance \mpr@tmpdim by \mpr@sep
   \fi
   }%
   \@rev
   \mpr@htovlist
   \ifmpr@center \hskip \wd\mpr@vlist\fi \box \mpr@vlist
   \fi
   \egroup
}

%%%%%%%%%%%%%%%%
%% BEGIN PATCH

%% Alternate solution for @hovbox so as to compute premises
%% in order of appearance.

\newcommand {\mpr@texbool}[1]
    {#1\let \bln@do \@firstoftwo \else \let \bln@do \@secondoftwo \fi
     \bln@do}
\def \mpr@ifpremise {\mpr@texbool {\ifmpr@premise}}
\newcommand {\mpr@assert}[2][]
   {\mpr@texbool{#2}{}{\PackageError {mathpartir}{#1}{\FATAL}}}
\newcommand {\mpr@avoid}[2][]
   {\mpr@texbool{#2}{\PackageError {mathpartir}{#1}{\FATAL}}{}}

%% Do not change this
\def \mpr@empty {}
\def \mpr@ifempty #1{%
  \def \@test {#1}\ifx \@test \mpr@empty \let \@do \@firstoftwo
  \else \let \@do \@secondoftwo \fi
  \@do}


%% Typesetting a rule item into a box
\def \mpr@ibox #1{\hbox {\strut \mpr@item {#1}}}

\newbox \mpr@tmpbox

\def \mpr@vskip@optional
  {\ifx \mpr@vskip \mpr@empty \else
   \hrule height 0em depth \mpr@vskip width 0em\fi}

%% Moving hlist to vlist (unless hlist is void)
\def \mpr@hontovlist
  {\ifvoid \mpr@hlist
   \else
     \setbox \mpr@vlist \vbox 
         {\hbox {\ifmpr@center \hskip -0.5\wd\mpr@hlist \fi
                 \unhbox\mpr@hlist}%
          \mpr@vskip@optional
          \unvbox\mpr@vlist}%
     \setbox \mpr@hlist \box\voidb@x
  \fi}

\def \mpr@rev@htovlist {%
  %% Pop \mpr@hlist into \mpr@vlist
  %% Warning! global setting of \box0.
  \mpr@assert {\ifmpr@premise}%
  \mpr@avoid [@rev@htovlist@begin] {\ifvoid \mpr@hlist}%
  \setbox0 \box\mpr@hlist
  \setbox \mpr@hlist \hbox
    {\unhbox0
     \setbox \mpr@hlist\lastbox \mpr@tmpdim \wd\mpr@hlist \relax
     \loop
       \setbox0 \lastbox
       \mpr@texbool{\ifvoid0}{\iffalse}{\mpr@tohlist \iftrue}%
     \repeat
     \ifvoid \mpr@hlist \else \mpr@hontovlist \fi
     \global \setbox0 \box\mpr@vlist
    }%
  \setbox\mpr@vlist\box0\relax
  \mpr@avoid[@rev@htovlist@end] {\ifvoid \mpr@hlist}%
  }

\def \mpr@hjoin #1#2{#1\hskip \mpr@sep #2}

\def \mpr@tohlist{%
  %% Pushes the hbox in \box0 into hlist
  %% Discharge @hlist into @vlist if needed
  %% \if@mprpremise drives the growing direction (T v.s. B).
  %% Maintain the width of @hlist plus in @tmpdim
  \mpr@avoid {\ifvoid0}%
  %% FIXME
  \mpr@tmpdim \wd\mpr@hlist
  \mpr@assert [\the \mpr@tmpdim =/= \the\wd\mpr@hlist]
      {\ifnum \mpr@tmpdim = \wd\mpr@hlist}%
  \advance \mpr@tmpdim by \mpr@sep
  \advance \mpr@tmpdim by \wd0
  \mpr@texbool {\ifdim \mpr@tmpdim > \hsize}
     {\mpr@hontovlist
      \setbox \mpr@hlist \box0
      \mpr@tmpdim \wd\mpr@hlist}%
     {\mpr@texbool {\ifvoid \mpr@hlist}
        {\setbox \mpr@hlist \box0}
        {\setbox \mpr@hlist \hbox {%
         \mpr@ifpremise
           {\mpr@hjoin {\box0}{\unhbox\mpr@hlist}}
           {\mpr@hjoin {\unhbox\mpr@hlist}{\box0}}}%
     }}%
  }

\def \mpr@next #1{%
  \mpr@ifempty{#1}
    {\mpr@ifpremise {\mpr@rev@htovlist}{\mpr@hontovlist}%
     \unvbox\mpr@vlist}%
    {\setbox0 \mpr@ibox {#1}%
     \mpr@ifpremise
        {\setbox \mpr@hlist \hbox {\unhbox\mpr@hlist \box0}}%
        {\mpr@tohlist}%
    }}

\def \mpr@hovbox@new #1#2{\hbox {%
  %% A boolean \mpr@premise... to signal T or B direction
  #1\relax
  \setbox \mpr@vlist \mpr@vbox {%
    \let \\ \relax
    \let \snoc \relax
    \setbox \mpr@hlist \box\voidb@x
    \setbox \mpr@vlist \box\voidb@x
    \expandafter \mpr@makelist #2\mpr@to \@tmp
    \let\\\mpr@next \@tmp\relax
    \mpr@ifpremise {\mpr@rev@htovlist}{\mpr@hontovlist}%
    \hbox {\box\mpr@vlist}%
  }%
  \ifmpr@center \hskip \wd\mpr@vlist\fi \box \mpr@vlist
  }}

\let \mpr@hovbox\mpr@hovbox@new

%% You may recover the old behavior by calling
%% \MprRecoverOlderVersion
\def \MprRecoverOlderVersion
   {\let \mpr@hovbox \mpr@hovbox@old}

%% END PATCH
%%%%%%%%%%%%%%%%

%%% INFERENCE RULES

\@ifundefined{@@over}{%
    \let\@@over\over % fallback if amsmath is not loaded
    \let\@@overwithdelims\overwithdelims
    \let\@@atop\atop \let\@@atopwithdelims\atopwithdelims
    \let\@@above\above \let\@@abovewithdelims\abovewithdelims
  }{}

%% The default

\def \mpr@@fraction #1#2{\hbox {\advance \hsize by -0.5em
    $\displaystyle {#1\mpr@over #2}$}}
\def \mpr@@nofraction #1#2{\hbox {\advance \hsize by -0.5em
    $\displaystyle {#1\@@atop #2}$}}

\let \mpr@fraction \mpr@@fraction

%% A generic solution to arrow

\def \mpr@@fractionaboveskip {0ex}
\def \mpr@@fractionbelowskip {0.22ex}

\def \mpr@make@fraction #1#2#3#4#5{\hbox {%
     \def \mpr@tail{#1}%
     \def \mpr@body{#2}%
     \def \mpr@head{#3}%
     \setbox1=\hbox{$#4$}\setbox2=\hbox{$#5$}%
     \setbox3=\hbox{$\mkern -3mu\mpr@body\mkern -3mu$}%
     \dimen0\ht3\advance\dimen0 by \dp3\relax
     \dimen0 0.5\dimen0\relax
     \advance \dimen0 by \mpr@@fractionaboveskip
     \setbox1=\hbox {\raise \dimen0 \box1}\relax
     \dimen0 -\dimen0\advance \dimen0 \mpr@@fractionaboveskip\dimen0 -\dimen0
     \advance \dimen0 by \mpr@@fractionbelowskip
     \setbox2=\hbox {\lower \dimen0 \box2}\relax
     \setbox0=\hbox {$\displaystyle {\box1 \atop \box2}$}%
     \dimen0=\wd0\box0
     \box0 \hskip -\dimen0\relax
     \hbox to \dimen0 {$%\color{blue}
       \mathrel{\mpr@tail}\joinrel
       \xleaders\hbox{\copy3}\hfil\joinrel\mathrel{\mpr@head}%
     $}}}

%% Old stuff should be removed in next version
\def \mpr@@nothing #1#2
    {$\lower 0.01pt \mpr@@nofraction {#1}{#2}$}
\def \mpr@@reduce #1#2{\hbox
    {$\lower 0.01pt \mpr@@fraction {#1}{#2}\mkern -15mu\rightarrow$}}
\def \mpr@@rewrite #1#2#3{\hbox
    {$\lower 0.01pt \mpr@@fraction {#2}{#3}\mkern -8mu#1$}}
\def \mpr@infercenter #1{\vcenter {\mpr@hovboxT{#1}}}


\def \mpr@infer@bindings{%
     \let \and \qquad
     \let \hva \mpr@hva
     \let \@rulename \mpr@empty
     \let \@rule@options \mpr@empty
     \let \mpr@over \@@over
}
\newcommand {\mpr@inferrule}[3][]
  {\bgroup
     \ifnum \linewidth<\hsize \hsize \linewidth\fi
     \mpr@rulelineskip
     \mpr@infer@bindings
     \everymath={\displaystyle}%
     \mpr@ifempty {#2}
        {\mpr@ifempty {#3}
          {\PackageWarning {mathpartir}
            {\string\inferrule\space empty arguments substituted}{}%
           \setbox0 \mpr@fraction {?}{?}}
          {\setbox0 \hbox {$\vcenter {\mpr@hovboxB{#3}}$}}}%
        {\mpr@ifempty {#3}
          {\setbox0 \hbox {$\vcenter {\mpr@hovboxT{#2}}$}}%
          {\setbox0 \mpr@fraction {\mpr@hovboxT{#2}}{\mpr@hovboxB{#3}}}}%
     \mpr@ifempty {#1}
        {\box0}
        {\vbox {\hbox {\DefTirName {#1}}\box0}}%
   \egroup}

\def \mpr@vdotfil #1{\vbox to #1{\leaders \hbox{$\cdot$} \vfil}}


%% Version for Hoare triples

\def \triple@hlinebox{\noalign{\setbox0\hbox {}\dp0 0.1ex\ht0 0.1ex\box0}}
\def \triple@hline {\triple@hlinebox\hline\triple@hlinebox}

\newcommand{\triplerule}[4][]
  {\bgroup
     \ifnum \linewidth<\hsize \hsize \linewidth\fi
     \mpr@rulelineskip
     \let \and \qquad
     \let \hva \mpr@hva
     \setbox0 \hbox {\begin{array}[b]{@{}c@{}}
     \mpr@hovboxT{#2}\cr\triple@hline
     \mpr@hovboxT{#3}\cr\triple@hline 
     \let \mpr@vbox \vtop \ht0 0em
     \setbox0 \strut \@tempdima \ht0
     \setbox0 \mpr@hovboxB{#4}\advance \@tempdima by -\ht0
     \setbox0 \hbox{\raise \@tempdima \box0}\box0
     \end{array}}%
   \def \@test {#1}\ifx \@test\empty \box0
   \else \vbox
      %%% Suggestion de Francois pour les etiquettes longues
      %%%   {\hbox to \wd0 {\RefTirName {#1}\hfil}\box0}\fi
      {\hbox {\DefTirName {#1}}\box0}\fi
   \egroup}
   

%% Keys that make sence in all kinds of rules
\def \mprset #1{\setkeys{mprset}{#1}}
\define@key {mprset}{andskip}[]{\mpr@andskip=#1}
\define@key {mprset}{lineskip}[]{\lineskip=#1}
\define@key {mprset}{lessskip}[]{\lineskip=0.5\lineskip}
\define@key {mprset}{flushleft}[]{\mpr@centerfalse}
\define@key {mprset}{center}[]{\mpr@centertrue}
\define@key {mprset}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite}
\define@key {mprset}{atop}[]{\let \mpr@fraction \mpr@@nofraction}
\define@key {mprset}{myfraction}[]{\let \mpr@fraction #1}
\define@key {mprset}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}}
\define@key {mprset}{defaultfraction}[]{\let \mpr@fraction \mpr@@fraction}
\define@key {mprset}{sep}{\def\mpr@sep{#1}}
\define@key {mprset}{fractionaboveskip}{\def\mpr@@fractionaboveskip{#1}}
\define@key {mprset}{fractionbelowskip}{\def\mpr@@fractionbelowskip{#1}}
\define@key {mprset}{style}[1]{\def\TirNameStyle{#1}}
\define@key {mprset}{rightstyle}[1]{\def\RightTirNameStyle{#1}}
\define@key {mprset}{leftstyle}[1]{\def\LeftTirNameStyle{#1}}
\define@key {mprset}{vskip}[1]{\def \mpr@vskip{#1}}

\newbox \mpr@right
\define@key {mpr}{flushleft}[]{\mpr@centerfalse}
\define@key {mpr}{center}[]{\mpr@centertrue}
\define@key {mpr}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite}
\define@key {mpr}{myfraction}[]{\let \mpr@fraction #1}
\define@key {mpr}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}}
\define@key {mpr}{width}{\hsize #1}
\define@key {mpr}{sep}{\def\mpr@sep{#1}}
\define@key {mpr}{before}{#1}
\define@key {mpr}{lab}{\let \DefTirName \LabTirName \def \mpr@rulename {#1}}
\define@key {mpr}{Lab}{\let \DefTirName \LabTirName \def \mpr@rulename {#1}}
\define@key {mpr}{style}[1]{\def\TirNameStyle{#1}}
\define@key {mpr}{rightstyle}[1]{\def\RightTirNameStyle{#1}}
\define@key {mpr}{leftstyle}[1]{\def\LeftTirNameStyle{#1}}
\define@key {mpr}{vskip}[1]{\def \mpr@vskip{#1}}
\define@key {mpr}{narrower}{\hsize #1\hsize}
\define@key {mpr}{leftskip}{\hskip -#1}
\define@key {mpr}{reduce}[]{\let \mpr@fraction \mpr@@reduce}
\define@key {mprset}{over}[\atop]{\def \mpr@@over{#1}}
\define@key {mpr}{rightskip}
  {\setbox \mpr@right \hbox {\unhbox \mpr@right \hskip -#1}}
\define@key {mpr}{LEFT}{\setbox0 \hbox {$#1$}\relax
     \advance \hsize by -\wd0\box0}

\define@key {mpr}{left}{\setbox0 \hbox {$\LeftTirName {#1}\;$}\relax
     \advance \hsize by -\wd0\box0}
\define@key {mpr}{Left}{\llap{$\LeftTirName {#1}\;$}}
\define@key {mpr}{right}
  {\setbox0 \hbox {$\;\RightTirName {#1}$}\relax \advance \hsize by -\wd0
   \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
\define@key {mpr}{RIGHT}
  {\setbox0 \hbox {$#1$}\relax \advance \hsize by -\wd0
   \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
\define@key {mpr}{Right}
  {\setbox \mpr@right \hbox {\unhbox \mpr@right \rlap {$\;\RightTirName {#1}$}}}
\define@key {mpr}{vdots}
  {\def \mpr@vdots {\mpr@vdotfil{#1}}}
  %% {\def \mpr@vdots {\@@atop \mpr@vdotfil{#1}}}
\define@key {mpr}{after}{\edef \mpr@after {\mpr@after #1}}
\define@key {mpr}{vcenter}[]{\mpr@vcentertrue}

\newif \ifmpr@vcenter \mpr@vcenterfalse
\newcommand \mpr@inferstar@ [3][]{\begingroup
  \setbox0 \hbox
     {\let \mpr@rulename \mpr@empty
      \let \mpr@vdots \mpr@empty
      \setbox \mpr@right \box\voidb@x%\hbox{}%
      \setkeys{mpr}{#1}%
      \mpr@texbool{\ifx \mpr@rulename \mpr@empty}
         {\let \mpr@call \mpr@inferrule}
         {\def \mpr@call {\mpr@inferrule [{\mpr@rulename}]}}%
      $\mpr@texbool{\ifx \mpr@vdots \mpr@empty}
         {\mpr@call {#2}{#3}}
         {\mpr@call {#2}{#3\\ \mpr@vdots}}%
       \box \mpr@right$%
      \ifmpr@vcenter \aftergroup \mpr@vcentertrue \fi}
  \ifmpr@vcenter
     \box0
  \else
     \setbox1 \hbox {\strut}
     \@tempdima \dp0 \advance \@tempdima by -\dp1
     \raise \@tempdima \box0
  \fi
  \endgroup}

\def \mpr@infer {\@ifnextchar *{\mpr@inferstar}{\mpr@inferrule}}
\newcommand \mpr@err@skipargs[3][]{}
\def \mpr@inferstar*{\ifmmode
    \let \@do \mpr@inferstar@
  \else
    \let \@do \mpr@err@skipargs
    \PackageError {mathpartir}
      {\string\inferrule* can only be used in math mode}{}%
  \fi \@do}

%%% Exports


\let \inferrule \mpr@infer

\@ifundefined {infer}{\let \infer \mpr@infer}{}

\def \TirNameStyle #1{\textsc{\small #1}}
\def \LeftTirNameStyle #1{\TirNameStyle {#1}}
\def \RightTirNameStyle #1{\TirNameStyle {#1}}

\def \lefttir@name #1{\hbox {\small \LeftTirNameStyle{#1}}}
\def \righttir@name #1{\hbox {\small \RightTirNameStyle{#1}}}
\let \TirName \lefttir@name
\let \LeftTirName \lefttir@name
\let \DefTirName \lefttir@name
\let \LabTirName \lefttir@name
\let \RightTirName \righttir@name

%%% Other Exports

\endinput
%%
%% End of file `mathpartir.sty'.