2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% Mathpartir --- Math Paragraph for Typesetting Inference Rules
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% Copyright (C) 2001, 2002, 2003, 2004, 2005 Didier R�my
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% Author : Didier Remy
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% Version : 1.2.0
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% Bug Reports : to author
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% Web Site : http://pauillac.inria.fr/~remy/latex/
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% Mathpartir is free software; you can redistribute it and/or modify
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% it under the terms of the GNU General Public License as published by
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% the Free Software Foundation; either version 2, or (at your option)
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% any later version.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% Mathpartir is distributed in the hope that it will be useful,
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% but WITHOUT ANY WARRANTY; without even the implied warranty of
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% GNU General Public License for more details
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% (http://pauillac.inria.fr/~remy/license/GPL).
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% File mathpartir.sty (LaTeX macros)
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\NeedsTeXFormat{LaTeX2e}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\ProvidesPackage{mathpartir}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann [2005/12/20 version 1.2.0 Math Paragraph for Typesetting Inference Rules]
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann%% Identification
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann%% Preliminary declarations
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\RequirePackage {keyval}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann%% More declarations
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann%% PART I: Typesetting maths in paragraphe mode
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann%% \newdimen \mpr@tmpdim
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann%% Dimens are a precious ressource. Uses seems to be local.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\let \mpr@tmpdim \@tempdima
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% To ensure hevea \hva compatibility, \hva should expands to nothing
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% in mathpar or in inferrule
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\let \mpr@hva \empty
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann%% normal paragraph parametters, should rather be taken dynamically
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\def \mpr@savepar {%
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \edef \MathparNormalpar
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann {\noexpand \lineskiplimit \the\lineskiplimit
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \noexpand \lineskip \the\lineskip}%
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\def \mpr@rulelineskip {\lineskiplimit=0.3em\lineskip=0.2em plus 0.1em}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\def \mpr@lesslineskip {\lineskiplimit=0.6em\lineskip=0.5em plus 0.2em}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\def \mpr@lineskip {\lineskiplimit=1.2em\lineskip=1.2em plus 0.2em}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\let \MathparLineskip \mpr@lineskip
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\def \mpr@paroptions {\MathparLineskip}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\let \mpr@prebindings \relax
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newskip \mpr@andskip \mpr@andskip 2em plus 0.5fil minus 0.5em
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\def \mpr@goodbreakand
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann {\hskip -\mpr@andskip \penalty -1000\hskip \mpr@andskip}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\def \mpr@and {\hskip \mpr@andskip}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\def \mpr@andcr {\penalty 50\mpr@and}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\def \mpr@cr {\penalty -10000\mpr@and}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\def \mpr@eqno #1{\mpr@andcr #1\hskip 0em plus -1fil \penalty 10}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\def \mpr@bindings {%
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \let \and \mpr@andcr
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \let \par \mpr@andcr
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \let \\\mpr@cr
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \let \eqno \mpr@eqno
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \let \hva \mpr@hva
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\let \MathparBindings \mpr@bindings
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% \@ifundefined {ignorespacesafterend}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% {\def \ignorespacesafterend {\aftergroup \ignorespaces}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newenvironment{mathpar}[1][]
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann {$$\mpr@savepar \parskip 0em \hsize \linewidth \centering
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \vbox \bgroup \mpr@prebindings \mpr@paroptions #1\ifmmode $\else
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \noindent $\displaystyle\fi
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \MathparBindings}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann {\unskip \ifmmode $\fi\egroup $$\ignorespacesafterend}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newenvironment{mathparpagebreakable}[1][]
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \mpr@savepar \parskip 0em \hsize \linewidth \centering
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \mpr@prebindings \mpr@paroptions #1%
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \vskip \abovedisplayskip \vskip -\lineskip%
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \ifmmode \else $\displaystyle\fi
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \MathparBindings
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \ifmmode $\fi \par\endgroup
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \vskip \belowdisplayskip
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \ignorespacesafterend}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% \def \math@mathpar #1{\setbox0 \hbox {$\displaystyle #1$}\ifnum
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% \wd0 < \hsize $$\box0$$\else \bmathpar #1\emathpar \fi}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\def \mathvbox@ #1{\hbox \bgroup \mpr@normallineskip
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \vbox \bgroup \tabskip 0em \let \\ \cr
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \halign \bgroup \hfil $##$\hfil\cr #1\crcr \egroup \egroup
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\def \mathhvbox@ #1{\setbox0 \hbox {\let \\\qquad $#1$}\ifnum \wd0 < \hsize
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \box0\else \mathvbox {#1}\fi}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann%% Part II -- operations on lists
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newtoks \mpr@lista
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newtoks \mpr@listb
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\long \def\mpr@cons #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann{#2}\edef #2{\the \mpr@lista \the \mpr@listb}}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\long \def\mpr@snoc #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann{#2}\edef #2{\the \mpr@listb\the\mpr@lista}}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\long \def \mpr@concat#1=#2\mpr@to#3{\mpr@lista \expandafter {#2}\mpr@listb
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\expandafter {#3}\edef #1{\the \mpr@listb\the\mpr@lista}}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\def \mpr@head #1\mpr@to #2{\expandafter \mpr@head@ #1\mpr@head@ #1#2}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\long \def \mpr@head@ #1#2\mpr@head@ #3#4{\def #4{#1}\def#3{#2}}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\def \mpr@flatten #1\mpr@to #2{\expandafter \mpr@flatten@ #1\mpr@flatten@ #1#2}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\long \def \mpr@flatten@ \\#1\\#2\mpr@flatten@ #3#4{\def #4{#1}\def #3{\\#2}}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\def \mpr@makelist #1\mpr@to #2{\def \mpr@all {#1}%
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \mpr@lista {\\}\mpr@listb \expandafter {\mpr@all}\edef \mpr@all {\the
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \mpr@lista \the \mpr@listb \the \mpr@lista}\let #2\empty
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \def \mpr@stripof ##1##2\mpr@stripend{\def \mpr@stripped{##2}}\loop
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \mpr@flatten \mpr@all \mpr@to \mpr@one
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \expandafter \mpr@snoc \mpr@one \mpr@to #2\expandafter \mpr@stripof
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \mpr@all \mpr@stripend
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \ifx \mpr@stripped \empty \let \mpr@isempty 0\else \let \mpr@isempty 1\fi
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \ifx 1\mpr@isempty
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\def \mpr@rev #1\mpr@to #2{\let \mpr@tmp \empty
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \def \\##1{\mpr@cons ##1\mpr@to \mpr@tmp}#1\let #2\mpr@tmp}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann%% Part III -- Type inference rules
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newif \if@premisse
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newbox \mpr@hlist
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newbox \mpr@vlist
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newif \ifmpr@center \mpr@centertrue
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\def \mpr@htovlist {%
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \setbox \mpr@hlist
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \hbox {\strut
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \ifmpr@center \hskip -0.5\wd\mpr@hlist\fi
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \unhbox \mpr@hlist}%
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \setbox \mpr@vlist
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \vbox {\if@premisse \box \mpr@hlist \unvbox \mpr@vlist
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \else \unvbox \mpr@vlist \box \mpr@hlist
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% \def \mpr@htovlist {%
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% \setbox \mpr@hlist
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% \hbox {\strut \hskip -0.5\wd\mpr@hlist \unhbox \mpr@hlist}%
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% \setbox \mpr@vlist
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% \vbox {\if@premisse \box \mpr@hlist \unvbox \mpr@vlist
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% \else \unvbox \mpr@vlist \box \mpr@hlist
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\def \mpr@item #1{$\displaystyle #1$}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\def \mpr@sep{2em}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\def \mpr@blank { }
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\def \mpr@hovbox #1#2{\hbox
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \ifx #1T\@premissetrue
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \else \ifx #1B\@premissefalse
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \PackageError{mathpartir}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann {Premisse orientation should either be T or B}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann {Fatal error in Package}%
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \def \@test {#2}\ifx \@test \mpr@blank\else
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \setbox \mpr@hlist \hbox {}%
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \setbox \mpr@vlist \vbox {}%
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \if@premisse \let \snoc \mpr@cons \else \let \snoc \mpr@snoc \fi
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \let \@hvlist \empty \let \@rev \empty
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \mpr@tmpdim 0em
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \expandafter \mpr@makelist #2\mpr@to \mpr@flat
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \if@premisse \mpr@rev \mpr@flat \mpr@to \@rev \else \let \@rev \mpr@flat \fi
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \def \@test {##1}\ifx \@test \empty
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \mpr@htovlist
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \mpr@tmpdim 0em %%% last bug fix not extensively checked
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \setbox0 \hbox{\mpr@item {##1}}\relax
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \advance \mpr@tmpdim by \wd0
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann %\mpr@tmpdim 1.02\mpr@tmpdim
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \ifnum \mpr@tmpdim < \hsize
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \ifnum \wd\mpr@hlist > 0
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \setbox \mpr@hlist
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \hbox {\unhbox0 \hskip \mpr@sep \unhbox \mpr@hlist}%
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \setbox \mpr@hlist
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \hbox {\unhbox \mpr@hlist \hskip \mpr@sep \unhbox0}%
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \setbox \mpr@hlist \hbox {\unhbox0}%
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \ifnum \wd \mpr@hlist > 0
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \mpr@htovlist
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \mpr@tmpdim \wd0
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \setbox \mpr@hlist \hbox {\unhbox0}%
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \advance \mpr@tmpdim by \mpr@sep
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \mpr@htovlist
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \ifmpr@center \hskip \wd\mpr@vlist\fi \box \mpr@vlist
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann%%% INFERENCE RULES
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\@ifundefined{@@over}{%
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \let\@@over\over % fallback if amsmath is not loaded
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \let\@@overwithdelims\overwithdelims
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \let\@@atop\atop \let\@@atopwithdelims\atopwithdelims
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \let\@@above\above \let\@@abovewithdelims\abovewithdelims
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann%% The default
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\def \mpr@@fraction #1#2{\hbox {\advance \hsize by -0.5em
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann $\displaystyle {#1\mpr@over #2}$}}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\def \mpr@@nofraction #1#2{\hbox {\advance \hsize by -0.5em
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann $\displaystyle {#1\@@atop #2}$}}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\let \mpr@fraction \mpr@@fraction
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann%% A generic solution to arrow
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\def \mpr@make@fraction #1#2#3#4#5{\hbox {%
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \def \mpr@tail{#1}%
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \def \mpr@body{#2}%
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \def \mpr@head{#3}%
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \setbox1=\hbox{$#4$}\setbox2=\hbox{$#5$}%
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \setbox3=\hbox{$\mkern -3mu\mpr@body\mkern -3mu$}%
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \setbox3=\hbox{$\mkern -3mu \mpr@body\mkern -3mu$}%
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \dimen0=\dp1\advance\dimen0 by \ht3\relax\dp1\dimen0\relax
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \dimen0=\ht2\advance\dimen0 by \dp3\relax\ht2\dimen0\relax
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \setbox0=\hbox {$\box1 \@@atop \box2$}%
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \dimen0=\wd0\box0
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \box0 \hskip -\dimen0\relax
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \hbox to \dimen0 {$%
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \mathrel{\mpr@tail}\joinrel
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \xleaders\hbox{\copy3}\hfil\joinrel\mathrel{\mpr@head}%
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann%% Old stuff should be removed in next version
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\def \mpr@@nothing #1#2
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann {$\lower 0.01pt \mpr@@nofraction {#1}{#2}$}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\def \mpr@@reduce #1#2{\hbox
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann {$\lower 0.01pt \mpr@@fraction {#1}{#2}\mkern -15mu\rightarrow$}}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\def \mpr@@rewrite #1#2#3{\hbox
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann {$\lower 0.01pt \mpr@@fraction {#2}{#3}\mkern -8mu#1$}}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\def \mpr@infercenter #1{\vcenter {\mpr@hovbox{T}{#1}}}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\def \mpr@empty {}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\def \mpr@inferrule
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \ifnum \linewidth<\hsize \hsize \linewidth\fi
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \mpr@rulelineskip
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \let \and \qquad
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \let \hva \mpr@hva
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \let \@rulename \mpr@empty
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \let \@rule@options \mpr@empty
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \let \mpr@over \@@over
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \mpr@inferrule@}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand {\mpr@inferrule@}[3][]
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann {\everymath={\displaystyle}%
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \def \@test {#2}\ifx \empty \@test
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \setbox0 \hbox {$\vcenter {\mpr@hovbox{B}{#3}}$}%
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \def \@test {#3}\ifx \empty \@test
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \setbox0 \hbox {$\vcenter {\mpr@hovbox{T}{#2}}$}%
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \setbox0 \mpr@fraction {\mpr@hovbox{T}{#2}}{\mpr@hovbox{B}{#3}}%
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \def \@test {#1}\ifx \@test\empty \box0
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann%%% Suggestion de Francois pour les etiquettes longues
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann%%% {\hbox to \wd0 {\RefTirName {#1}\hfil}\box0}\fi
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann {\hbox {\RefTirName {#1}}\box0}\fi
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\def \mpr@vdotfil #1{\vbox to #1{\leaders \hbox{$\cdot$} \vfil}}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% They are two forms
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% \inferrule [label]{[premisses}{conclusions}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% \inferrule* [options]{[premisses}{conclusions}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% Premisses and conclusions are lists of elements separated by \\
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% Each \\ produces a break, attempting horizontal breaks if possible,
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% and vertical breaks if needed.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% An empty element obtained by \\\\ produces a vertical break in all cases.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% The former rule is aligned on the fraction bar.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% The optional label appears on top of the rule
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% The second form to be used in a derivation tree is aligned on the last
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% line of its conclusion
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% The second form can be parameterized, using the key=val interface. The
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% folloiwng keys are recognized:
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% width set the width of the rule to val
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% narrower set the width of the rule to val\hsize
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% before execute val at the beginning/left
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% lab put a label [Val] on top of the rule
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% lskip add negative skip on the right
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% left put a left label [Val]
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% Left put a left label [Val], ignoring its width
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% right put a right label [Val]
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% Right put a right label [Val], ignoring its width
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% leftskip skip negative space on the left-hand side
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% rightskip skip negative space on the right-hand side
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% vdots lift the rule by val and fill vertical space with dots
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% after execute val at the end/right
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% Note that most options must come in this order to avoid strange
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% typesetting (in particular leftskip must preceed left and Left and
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% rightskip must follow Right or right; vdots must come last
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% or be only followed by rightskip.
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann%% Keys that make sence in all kinds of rules
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\def \mprset #1{\setkeys{mprset}{#1}}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\define@key {mprset}{andskip}[]{\mpr@andskip=#1}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\define@key {mprset}{lineskip}[]{\lineskip=#1}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\define@key {mprset}{flushleft}[]{\mpr@centerfalse}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\define@key {mprset}{center}[]{\mpr@centertrue}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\define@key {mprset}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\define@key {mprset}{atop}[]{\let \mpr@fraction \mpr@@nofraction}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\define@key {mprset}{myfraction}[]{\let \mpr@fraction #1}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\define@key {mprset}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\define@key {mprset}{sep}{\def\mpr@sep{#1}}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newbox \mpr@right
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\define@key {mpr}{flushleft}[]{\mpr@centerfalse}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\define@key {mpr}{center}[]{\mpr@centertrue}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\define@key {mpr}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\define@key {mpr}{myfraction}[]{\let \mpr@fraction #1}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\define@key {mpr}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \advance \hsize by -\wd0\box0}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\define@key {mpr}{width}{\hsize #1}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\define@key {mpr}{sep}{\def\mpr@sep{#1}}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\define@key {mpr}{before}{#1}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\define@key {mpr}{lab}{\let \RefTirName \TirName \def \mpr@rulename {#1}}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\define@key {mpr}{Lab}{\let \RefTirName \TirName \def \mpr@rulename {#1}}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\define@key {mpr}{narrower}{\hsize #1\hsize}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\define@key {mpr}{leftskip}{\hskip -#1}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\define@key {mpr}{reduce}[]{\let \mpr@fraction \mpr@@reduce}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\define@key {mpr}{rightskip}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann {\setbox \mpr@right \hbox {\unhbox \mpr@right \hskip -#1}}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\define@key {mpr}{LEFT}{\setbox0 \hbox {$#1$}\relax
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \advance \hsize by -\wd0\box0}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \advance \hsize by -\wd0\box0}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\define@key {mpr}{Left}{\llap{$\TirName {#1}\;$}}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\define@key {mpr}{right}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann {\setbox0 \hbox {$\;\TirName {#1}$}\relax \advance \hsize by -\wd0
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\define@key {mpr}{RIGHT}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann {\setbox0 \hbox {$#1$}\relax \advance \hsize by -\wd0
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\define@key {mpr}{Right}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann {\setbox \mpr@right \hbox {\unhbox \mpr@right \rlap {$\;\TirName {#1}$}}}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\define@key {mpr}{vdots}{\def \mpr@vdots {\@@atop \mpr@vdotfil{#1}}}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\define@key {mpr}{after}{\edef \mpr@after {\mpr@after #1}}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand \mpr@inferstar@ [3][]{\setbox0
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \hbox {\let \mpr@rulename \mpr@empty \let \mpr@vdots \relax
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \setbox \mpr@right \hbox{}%
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann $\setkeys{mpr}{#1}%
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \ifx \mpr@rulename \mpr@empty \mpr@inferrule {#2}{#3}\else
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \mpr@inferrule [{\mpr@rulename}]{#2}{#3}\fi
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \box \mpr@right \mpr@vdots$}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \setbox1 \hbox {\strut}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \@tempdima \dp0 \advance \@tempdima by -\dp1
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \raise \@tempdima \box0}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\def \mpr@infer {\@ifnextchar *{\mpr@inferstar}{\mpr@inferrule}}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\newcommand \mpr@err@skipargs[3][]{}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\def \mpr@inferstar*{\ifmmode
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \let \@do \mpr@inferstar@
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \let \@do \mpr@err@skipargs
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann \PackageError {mathpartir}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann {\string\inferrule* can only be used in math mode}{}%
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% Envirnonment mathpar
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\let \inferrule \mpr@infer
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% make a short name \infer is not already defined
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\@ifundefined {infer}{\let \infer \mpr@infer}{}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\def \TirNameStyle #1{\small \textsc{#1}}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\def \tir@name #1{\hbox {\small \TirNameStyle{#1}}}
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\let \TirName \tir@name
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\let \DefTirName \TirName
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann\let \RefTirName \TirName
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann%%% Other Exports
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% \let \listcons \mpr@cons
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% \let \listsnoc \mpr@snoc
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% \let \listhead \mpr@head
2450a4210dee64b064499a3a1154129bdfc74981Daniel Hausmann% \let \listmake \mpr@makelist