author | nipkow |
Mon, 29 Nov 2004 11:12:19 +0100 | |
changeset 15337 | 628d87767434 |
child 16075 | 8852058ecf8d |
permissions | -rw-r--r-- |
nipkow@15337 | 1 |
%% |
nipkow@15337 | 2 |
%% This is the original source file mathpar.sty |
nipkow@15337 | 3 |
%% |
nipkow@15337 | 4 |
%% Package `mathpar' to use with LaTeX 2e |
nipkow@15337 | 5 |
%% Copyright Didier Remy, all rights reserved. |
nipkow@15337 | 6 |
\NeedsTeXFormat{LaTeX2e} |
nipkow@15337 | 7 |
\ProvidesPackage{mathpartir} |
nipkow@15337 | 8 |
[2001/23/02 v0.92 Math Paragraph for Type Inference Rules] |
nipkow@15337 | 9 |
|
nipkow@15337 | 10 |
%% |
nipkow@15337 | 11 |
|
nipkow@15337 | 12 |
%% Identification |
nipkow@15337 | 13 |
%% Preliminary declarations |
nipkow@15337 | 14 |
|
nipkow@15337 | 15 |
\RequirePackage {keyval} |
nipkow@15337 | 16 |
|
nipkow@15337 | 17 |
%% Options |
nipkow@15337 | 18 |
%% More declarations |
nipkow@15337 | 19 |
|
nipkow@15337 | 20 |
%% PART I: Typesetting maths in paragraphe mode |
nipkow@15337 | 21 |
|
nipkow@15337 | 22 |
\newdimen \mpr@tmpdim |
nipkow@15337 | 23 |
|
nipkow@15337 | 24 |
% To ensure hevea \hva compatibility, \hva should expands to nothing |
nipkow@15337 | 25 |
% in mathpar or in mathrule |
nipkow@15337 | 26 |
\let \mpr@hva \empty |
nipkow@15337 | 27 |
|
nipkow@15337 | 28 |
%% normal paragraph parametters, should rather be taken dynamically |
nipkow@15337 | 29 |
\def \mpr@savepar {% |
nipkow@15337 | 30 |
\edef \MathparNormalpar |
nipkow@15337 | 31 |
{\noexpand \lineskiplimit \the\lineskiplimit |
nipkow@15337 | 32 |
\noexpand \lineski \the\lineskip}% |
nipkow@15337 | 33 |
} |
nipkow@15337 | 34 |
|
nipkow@15337 | 35 |
\def \mpr@rulelineskip {\lineskiplimit=0.3em\lineskip=0.2em plus 0.1em} |
nipkow@15337 | 36 |
\def \mpr@lesslineskip {\lineskiplimit=0.6em\lineskip=0.5em plus 0.2em} |
nipkow@15337 | 37 |
\def \mpr@lineskip {\lineskiplimit=1.2em\lineskip=1.2em plus 0.2em} |
nipkow@15337 | 38 |
\let \MathparLineskip \mpr@lineskip |
nipkow@15337 | 39 |
\def \mpr@paroptions {\MathparLineskip} |
nipkow@15337 | 40 |
\let \mpr@prebindings \relax |
nipkow@15337 | 41 |
|
nipkow@15337 | 42 |
\newskip \mpr@andskip \mpr@andskip 2em plus 0.5fil minus 0.5em |
nipkow@15337 | 43 |
|
nipkow@15337 | 44 |
\def \mpr@goodbreakand |
nipkow@15337 | 45 |
{\hskip -\mpr@andskip \penalty -1000\hskip \mpr@andskip} |
nipkow@15337 | 46 |
\def \mpr@and {\hskip \mpr@andskip} |
nipkow@15337 | 47 |
\def \mpr@andcr {\penalty 50\mpr@and} |
nipkow@15337 | 48 |
\def \mpr@cr {\penalty -10000\mpr@and} |
nipkow@15337 | 49 |
\def \mpr@eqno #1{\mpr@andcr #1\hskip 0em plus -1fil \penalty 10} |
nipkow@15337 | 50 |
|
nipkow@15337 | 51 |
\def \mpr@bindings {% |
nipkow@15337 | 52 |
\let \and \mpr@andcr |
nipkow@15337 | 53 |
\let \par \mpr@andcr |
nipkow@15337 | 54 |
\let \\\mpr@cr |
nipkow@15337 | 55 |
\let \eqno \mpr@eqno |
nipkow@15337 | 56 |
\let \hva \mpr@hva |
nipkow@15337 | 57 |
} |
nipkow@15337 | 58 |
\let \MathparBindings \mpr@bindings |
nipkow@15337 | 59 |
|
nipkow@15337 | 60 |
\newenvironment{mathpar}[1][] |
nipkow@15337 | 61 |
{$$\mpr@savepar \parskip 0em \hsize \linewidth \centering |
nipkow@15337 | 62 |
\vbox \bgroup \mpr@prebindings \mpr@paroptions #1\ifmmode $\else |
nipkow@15337 | 63 |
\noindent $\displaystyle\fi |
nipkow@15337 | 64 |
\MathparBindings} |
nipkow@15337 | 65 |
{\unskip \ifmmode $\fi\egroup $$\ignorespacesafterend} |
nipkow@15337 | 66 |
|
nipkow@15337 | 67 |
% \def \math@mathpar #1{\setbox0 \hbox {$\displaystyle #1$}\ifnum |
nipkow@15337 | 68 |
% \wd0 < \hsize $$\box0$$\else \bmathpar #1\emathpar \fi} |
nipkow@15337 | 69 |
|
nipkow@15337 | 70 |
%%% HOV BOXES |
nipkow@15337 | 71 |
|
nipkow@15337 | 72 |
\def \mathvbox@ #1{\hbox \bgroup \mpr@normallineskip |
nipkow@15337 | 73 |
\vbox \bgroup \tabskip 0em \let \\ \cr |
nipkow@15337 | 74 |
\halign \bgroup \hfil $##$\hfil\cr #1\crcr \egroup \egroup |
nipkow@15337 | 75 |
\egroup} |
nipkow@15337 | 76 |
|
nipkow@15337 | 77 |
\def \mathhvbox@ #1{\setbox0 \hbox {\let \\\qquad $#1$}\ifnum \wd0 < \hsize |
nipkow@15337 | 78 |
\box0\else \mathvbox {#1}\fi} |
nipkow@15337 | 79 |
|
nipkow@15337 | 80 |
|
nipkow@15337 | 81 |
%% Part II -- operations on lists |
nipkow@15337 | 82 |
|
nipkow@15337 | 83 |
\newtoks \mpr@lista |
nipkow@15337 | 84 |
\newtoks \mpr@listb |
nipkow@15337 | 85 |
|
nipkow@15337 | 86 |
\long \def\mpr@cons #1\to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter |
nipkow@15337 | 87 |
{#2}\edef #2{\the \mpr@lista \the \mpr@listb}} |
nipkow@15337 | 88 |
|
nipkow@15337 | 89 |
\long \def\mpr@snoc #1\to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter |
nipkow@15337 | 90 |
{#2}\edef #2{\the \mpr@listb\the\mpr@lista}} |
nipkow@15337 | 91 |
|
nipkow@15337 | 92 |
\long \def \mpr@concat#1=#2\to#3{\mpr@lista \expandafter {#2}\mpr@listb |
nipkow@15337 | 93 |
\expandafter {#3}\edef #1{\the \mpr@listb\the\mpr@lista}} |
nipkow@15337 | 94 |
|
nipkow@15337 | 95 |
\def \mpr@head #1\to #2{\expandafter \mpr@head@ #1\mpr@head@ #1#2} |
nipkow@15337 | 96 |
\long \def \mpr@head@ #1#2\mpr@head@ #3#4{\def #4{#1}\def#3{#2}} |
nipkow@15337 | 97 |
|
nipkow@15337 | 98 |
\def \mpr@flatten #1\to #2{\expandafter \mpr@flatten@ #1\mpr@flatten@ #1#2} |
nipkow@15337 | 99 |
\long \def \mpr@flatten@ \\#1\\#2\mpr@flatten@ #3#4{\def #4{#1}\def #3{\\#2}} |
nipkow@15337 | 100 |
|
nipkow@15337 | 101 |
\def \mpr@makelist #1\to #2{\def \mpr@all {#1}% |
nipkow@15337 | 102 |
\mpr@lista {\\}\mpr@listb \expandafter {\mpr@all}\edef \mpr@all {\the |
nipkow@15337 | 103 |
\mpr@lista \the \mpr@listb \the \mpr@lista}\let #2\empty |
nipkow@15337 | 104 |
\def \mpr@stripof ##1##2\mpr@stripend{\def \mpr@stripped{##2}}\loop |
nipkow@15337 | 105 |
\mpr@flatten \mpr@all \to \mpr@one |
nipkow@15337 | 106 |
\expandafter \mpr@snoc \mpr@one \to #2\expandafter \mpr@stripof |
nipkow@15337 | 107 |
\mpr@all \mpr@stripend |
nipkow@15337 | 108 |
\ifx \mpr@stripped \empty \let \mpr@isempty 0\else \let \mpr@isempty 1\fi |
nipkow@15337 | 109 |
\ifx 1\mpr@isempty |
nipkow@15337 | 110 |
\repeat |
nipkow@15337 | 111 |
} |
nipkow@15337 | 112 |
|
nipkow@15337 | 113 |
%% Part III -- Type inference rules |
nipkow@15337 | 114 |
|
nipkow@15337 | 115 |
\def \mpr@rev #1\to #2{\let \mpr@tmp \empty |
nipkow@15337 | 116 |
\def \\##1{\mpr@cons ##1\to \mpr@tmp}#1\let #2\mpr@tmp} |
nipkow@15337 | 117 |
|
nipkow@15337 | 118 |
\newif \if@premisse |
nipkow@15337 | 119 |
\newbox \mpr@hlist |
nipkow@15337 | 120 |
\newbox \mpr@vlist |
nipkow@15337 | 121 |
\newif \ifmpr@center \mpr@centertrue |
nipkow@15337 | 122 |
\def \mpr@htovlist {% |
nipkow@15337 | 123 |
\setbox \mpr@hlist |
nipkow@15337 | 124 |
\hbox {\strut |
nipkow@15337 | 125 |
\ifmpr@center \hskip -0.5\wd\mpr@hlist\fi |
nipkow@15337 | 126 |
\unhbox \mpr@hlist}% |
nipkow@15337 | 127 |
\setbox \mpr@vlist |
nipkow@15337 | 128 |
\vbox {\if@premisse \box \mpr@hlist \unvbox \mpr@vlist |
nipkow@15337 | 129 |
\else \unvbox \mpr@vlist \box \mpr@hlist |
nipkow@15337 | 130 |
\fi}% |
nipkow@15337 | 131 |
} |
nipkow@15337 | 132 |
% OLD version |
nipkow@15337 | 133 |
% \def \mpr@htovlist {% |
nipkow@15337 | 134 |
% \setbox \mpr@hlist |
nipkow@15337 | 135 |
% \hbox {\strut \hskip -0.5\wd\mpr@hlist \unhbox \mpr@hlist}% |
nipkow@15337 | 136 |
% \setbox \mpr@vlist |
nipkow@15337 | 137 |
% \vbox {\if@premisse \box \mpr@hlist \unvbox \mpr@vlist |
nipkow@15337 | 138 |
% \else \unvbox \mpr@vlist \box \mpr@hlist |
nipkow@15337 | 139 |
% \fi}% |
nipkow@15337 | 140 |
% } |
nipkow@15337 | 141 |
|
nipkow@15337 | 142 |
|
nipkow@15337 | 143 |
|
nipkow@15337 | 144 |
|
nipkow@15337 | 145 |
\def \mpr@blank { } |
nipkow@15337 | 146 |
\def \mpr@hovbox #1#2{\hbox |
nipkow@15337 | 147 |
\bgroup |
nipkow@15337 | 148 |
\ifx #1T\@premissetrue |
nipkow@15337 | 149 |
\else \ifx #1B\@premissefalse |
nipkow@15337 | 150 |
\else |
nipkow@15337 | 151 |
\PackageError{mathpartir} |
nipkow@15337 | 152 |
{Premisse orientation should either be P or B} |
nipkow@15337 | 153 |
{Fatal error in Package}% |
nipkow@15337 | 154 |
\fi \fi |
nipkow@15337 | 155 |
\def \@test {#2}\ifx \@test \mpr@blank\else |
nipkow@15337 | 156 |
\setbox \mpr@hlist \hbox {}% |
nipkow@15337 | 157 |
\setbox \mpr@vlist \vbox {}% |
nipkow@15337 | 158 |
\if@premisse \let \snoc \mpr@cons \else \let \snoc \mpr@snoc \fi |
nipkow@15337 | 159 |
\let \@hvlist \empty \let \@rev \empty |
nipkow@15337 | 160 |
\mpr@tmpdim 0em |
nipkow@15337 | 161 |
\expandafter \mpr@makelist #2\to \mpr@flat |
nipkow@15337 | 162 |
\if@premisse \mpr@rev \mpr@flat \to \@rev \else \let \@rev \mpr@flat \fi |
nipkow@15337 | 163 |
\def \\##1{% |
nipkow@15337 | 164 |
\def \@test {##1}\ifx \@test \empty |
nipkow@15337 | 165 |
\mpr@htovlist |
nipkow@15337 | 166 |
\mpr@tmpdim 0em %%% last bug fix not extensively checked |
nipkow@15337 | 167 |
\else |
nipkow@15337 | 168 |
\setbox0 \hbox{$\displaystyle {##1}$}\relax |
nipkow@15337 | 169 |
\advance \mpr@tmpdim by \wd0 |
nipkow@15337 | 170 |
%\mpr@tmpdim 1.02\mpr@tmpdim |
nipkow@15337 | 171 |
\ifnum \mpr@tmpdim < \hsize |
nipkow@15337 | 172 |
\ifnum \wd\mpr@hlist > 0 |
nipkow@15337 | 173 |
\if@premisse |
nipkow@15337 | 174 |
\setbox \mpr@hlist \hbox {\unhbox0 \qquad \unhbox \mpr@hlist}% |
nipkow@15337 | 175 |
\else |
nipkow@15337 | 176 |
\setbox \mpr@hlist \hbox {\unhbox \mpr@hlist \qquad \unhbox0}% |
nipkow@15337 | 177 |
\fi |
nipkow@15337 | 178 |
\else |
nipkow@15337 | 179 |
\setbox \mpr@hlist \hbox {\unhbox0}% |
nipkow@15337 | 180 |
\fi |
nipkow@15337 | 181 |
\else |
nipkow@15337 | 182 |
\ifnum \wd \mpr@hlist > 0 |
nipkow@15337 | 183 |
\mpr@htovlist |
nipkow@15337 | 184 |
\mpr@tmpdim \wd0 |
nipkow@15337 | 185 |
\fi |
nipkow@15337 | 186 |
\setbox \mpr@hlist \hbox {\unhbox0}% |
nipkow@15337 | 187 |
\fi |
nipkow@15337 | 188 |
\advance \mpr@tmpdim by 2em |
nipkow@15337 | 189 |
\fi |
nipkow@15337 | 190 |
}% |
nipkow@15337 | 191 |
\@rev |
nipkow@15337 | 192 |
\mpr@htovlist |
nipkow@15337 | 193 |
\ifmpr@center \hskip \wd\mpr@vlist\fi \box \mpr@vlist |
nipkow@15337 | 194 |
\fi |
nipkow@15337 | 195 |
\egroup |
nipkow@15337 | 196 |
} |
nipkow@15337 | 197 |
|
nipkow@15337 | 198 |
%%% INFERENCE RULES |
nipkow@15337 | 199 |
|
nipkow@15337 | 200 |
\@ifundefined{@@over}{% |
nipkow@15337 | 201 |
\let\@@over\over % fallback if amsmath is not loaded |
nipkow@15337 | 202 |
\let\@@overwithdelims\overwithdelims |
nipkow@15337 | 203 |
\let\@@atop\atop \let\@@atopwithdelims\atopwithdelims |
nipkow@15337 | 204 |
\let\@@above\above \let\@@abovewithdelims\abovewithdelims |
nipkow@15337 | 205 |
}{} |
nipkow@15337 | 206 |
|
nipkow@15337 | 207 |
|
nipkow@15337 | 208 |
\def \mpr@@fraction #1#2{\hbox {\advance \hsize by -0.5em |
nipkow@15337 | 209 |
$\displaystyle {#1\@@over #2}$}} |
nipkow@15337 | 210 |
\let \mpr@fraction \mpr@@fraction |
nipkow@15337 | 211 |
\def \mpr@@reduce #1#2{\hbox |
nipkow@15337 | 212 |
{$\lower 0.01pt \mpr@@fraction {#1}{#2}\mkern -15mu\rightarrow$}} |
nipkow@15337 | 213 |
\def \mpr@infercenter #1{\vcenter {\mpr@hovbox{T}{#1}}} |
nipkow@15337 | 214 |
|
nipkow@15337 | 215 |
\def \mpr@empty {} |
nipkow@15337 | 216 |
\def \mpr@inferrule |
nipkow@15337 | 217 |
{\bgroup |
nipkow@15337 | 218 |
\mpr@rulelineskip |
nipkow@15337 | 219 |
\let \and \qquad |
nipkow@15337 | 220 |
\let \hva \mpr@hva |
nipkow@15337 | 221 |
\let \@rulename \mpr@empty |
nipkow@15337 | 222 |
\let \@rule@options \mpr@empty |
nipkow@15337 | 223 |
\mpr@inferrule@} |
nipkow@15337 | 224 |
\newcommand {\mpr@inferrule@}[3][] |
nipkow@15337 | 225 |
{\everymath={\displaystyle}% |
nipkow@15337 | 226 |
\def \@test {#2}\ifx \empty \@test |
nipkow@15337 | 227 |
\setbox0 \hbox {$\vcenter {\mpr@hovbox{B}{#3}}$}% |
nipkow@15337 | 228 |
\else |
nipkow@15337 | 229 |
\def \@test {#3}\ifx \empty \@test |
nipkow@15337 | 230 |
\setbox0 \hbox {$\vcenter {\mpr@hovbox{T}{#2}}$}% |
nipkow@15337 | 231 |
\else |
nipkow@15337 | 232 |
\setbox0 \mpr@fraction {\mpr@hovbox{T}{#2}}{\mpr@hovbox{B}{#3}}% |
nipkow@15337 | 233 |
\fi \fi |
nipkow@15337 | 234 |
\def \@test {#1}\ifx \@test\empty \box0 |
nipkow@15337 | 235 |
\else \vbox |
nipkow@15337 | 236 |
%%% Suggestion de Francois pour les etiquettes longues |
nipkow@15337 | 237 |
%%% {\hbox to \wd0 {\TirName {#1}\hfil}\box0}\fi |
nipkow@15337 | 238 |
{\hbox {\TirName {#1}}\box0}\fi |
nipkow@15337 | 239 |
\egroup} |
nipkow@15337 | 240 |
|
nipkow@15337 | 241 |
\def \mpr@vdotfil #1{\vbox to #1{\leaders \hbox{$\cdot$} \vfil}} |
nipkow@15337 | 242 |
|
nipkow@15337 | 243 |
% They are two forms |
nipkow@15337 | 244 |
% \mathrule [label]{[premisses}{conclusions} |
nipkow@15337 | 245 |
% or |
nipkow@15337 | 246 |
% \mathrule* [options]{[premisses}{conclusions} |
nipkow@15337 | 247 |
% |
nipkow@15337 | 248 |
% Premisses and conclusions are lists of elements separated by \\ |
nipkow@15337 | 249 |
% Each \\ produces a break, attempting horizontal breaks if possible, |
nipkow@15337 | 250 |
% and vertical breaks if needed. |
nipkow@15337 | 251 |
% |
nipkow@15337 | 252 |
% An empty element obtained by \\\\ produces a vertical break in all cases. |
nipkow@15337 | 253 |
% |
nipkow@15337 | 254 |
% The former rule is aligned on the fraction bar. |
nipkow@15337 | 255 |
% The optional label appears on top of the rule |
nipkow@15337 | 256 |
% The second form to be used in a derivation tree is aligned on the last |
nipkow@15337 | 257 |
% line of its conclusion |
nipkow@15337 | 258 |
% |
nipkow@15337 | 259 |
% The second form can be parameterized, using the key=val interface. The |
nipkow@15337 | 260 |
% folloiwng keys are recognized: |
nipkow@15337 | 261 |
% |
nipkow@15337 | 262 |
% width set the width of the rule to val |
nipkow@15337 | 263 |
% narrower set the width of the rule to val\hsize |
nipkow@15337 | 264 |
% before execute val at the beginning/left |
nipkow@15337 | 265 |
% lab put a label [Val] on top of the rule |
nipkow@15337 | 266 |
% lskip add negative skip on the right |
nipkow@15337 | 267 |
% llab put a left label [Val], ignoring its width |
nipkow@15337 | 268 |
% left put a left label [Val] |
nipkow@15337 | 269 |
% right put a right label [Val] |
nipkow@15337 | 270 |
% rlab put a right label [Val], ignoring its width |
nipkow@15337 | 271 |
% rskip add negative skip on the left |
nipkow@15337 | 272 |
% vdots lift the rule by val and fill vertical space with dots |
nipkow@15337 | 273 |
% after execute val at the end/right |
nipkow@15337 | 274 |
% |
nipkow@15337 | 275 |
% Note that most options must come in this order to avoid strange |
nipkow@15337 | 276 |
% typesetting (in particular lskip must preceed left and llab and |
nipkow@15337 | 277 |
% rskip must follow rlab or right; vdots must come last or be followed by |
nipkow@15337 | 278 |
% rskip. |
nipkow@15337 | 279 |
% |
nipkow@15337 | 280 |
|
nipkow@15337 | 281 |
\define@key {mprset}{flushleft}[]{\mpr@centerfalse} |
nipkow@15337 | 282 |
\define@key {mprset}{center}[]{\mpr@centertrue} |
nipkow@15337 | 283 |
\def \mprset #1{\setkeys{mprset}{#1}} |
nipkow@15337 | 284 |
|
nipkow@15337 | 285 |
\newbox \mpr@right |
nipkow@15337 | 286 |
\define@key {mpr}{flushleft}[]{\mpr@centerfalse} |
nipkow@15337 | 287 |
\define@key {mpr}{center}[]{\mpr@centertrue} |
nipkow@15337 | 288 |
\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax |
nipkow@15337 | 289 |
\advance \hsize by -\wd0\box0} |
nipkow@15337 | 290 |
\define@key {mpr}{width}{\hsize #1} |
nipkow@15337 | 291 |
\define@key {mpr}{before}{#1} |
nipkow@15337 | 292 |
\define@key {mpr}{lab}{\def \mpr@rulename {[#1]}} |
nipkow@15337 | 293 |
\define@key {mpr}{Lab}{\def \mpr@rulename {#1}} |
nipkow@15337 | 294 |
\define@key {mpr}{narrower}{\hsize #1\hsize} |
nipkow@15337 | 295 |
\define@key {mpr}{leftskip}{\hskip -#1} |
nipkow@15337 | 296 |
\define@key {mpr}{reduce}[]{\let \mpr@fraction \mpr@@reduce} |
nipkow@15337 | 297 |
\define@key {mpr}{rightskip} |
nipkow@15337 | 298 |
{\setbox \mpr@right \hbox {\unhbox \mpr@right \hskip -#1}} |
nipkow@15337 | 299 |
\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax |
nipkow@15337 | 300 |
\advance \hsize by -\wd0\box0} |
nipkow@15337 | 301 |
\define@key {mpr}{Left}{\llap{$\TirName {#1}\;$}} |
nipkow@15337 | 302 |
\define@key {mpr}{right} |
nipkow@15337 | 303 |
{\setbox0 \hbox {$\;\TirName {#1}$}\relax \advance \hsize by -\wd0 |
nipkow@15337 | 304 |
\setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}} |
nipkow@15337 | 305 |
\define@key {mpr}{Right} |
nipkow@15337 | 306 |
{\setbox \mpr@right \hbox {\unhbox \mpr@right \rlap {$\;\TirName {#1}$}}} |
nipkow@15337 | 307 |
\define@key {mpr}{vdots}{\def \mpr@vdots {\@@atop \mpr@vdotfil{#1}}} |
nipkow@15337 | 308 |
\define@key {mpr}{after}{\edef \mpr@after {\mpr@after #1}} |
nipkow@15337 | 309 |
|
nipkow@15337 | 310 |
\newdimen \rule@dimen |
nipkow@15337 | 311 |
\newcommand \mpr@inferstar@ [3][]{\setbox0 |
nipkow@15337 | 312 |
\hbox {\let \mpr@rulename \mpr@empty \let \mpr@vdots \relax |
nipkow@15337 | 313 |
\setbox \mpr@right \hbox{}% |
nipkow@15337 | 314 |
$\setkeys{mpr}{#1}% |
nipkow@15337 | 315 |
\ifx \mpr@rulename \mpr@empty \mpr@inferrule {#2}{#3}\else |
nipkow@15337 | 316 |
\mpr@inferrule [{\mpr@rulename}]{#2}{#3}\fi |
nipkow@15337 | 317 |
\box \mpr@right \mpr@vdots$} |
nipkow@15337 | 318 |
\setbox1 \hbox {\strut} |
nipkow@15337 | 319 |
\rule@dimen \dp0 \advance \rule@dimen by -\dp1 |
nipkow@15337 | 320 |
\raise \rule@dimen \box0} |
nipkow@15337 | 321 |
|
nipkow@15337 | 322 |
\def \mpr@infer {\@ifnextchar *{\mpr@inferstar}{\mpr@inferrule}} |
nipkow@15337 | 323 |
\newcommand \mpr@err@skipargs[3][]{} |
nipkow@15337 | 324 |
\def \mpr@inferstar*{\ifmmode |
nipkow@15337 | 325 |
\let \@do \mpr@inferstar@ |
nipkow@15337 | 326 |
\else |
nipkow@15337 | 327 |
\let \@do \mpr@err@skipargs |
nipkow@15337 | 328 |
\PackageError {mathpartir} |
nipkow@15337 | 329 |
{\string\inferrule* can only be used in math mode}{}% |
nipkow@15337 | 330 |
\fi \@do} |
nipkow@15337 | 331 |
|
nipkow@15337 | 332 |
|
nipkow@15337 | 333 |
%%% Exports |
nipkow@15337 | 334 |
|
nipkow@15337 | 335 |
% Envirnonment mathpar |
nipkow@15337 | 336 |
|
nipkow@15337 | 337 |
\let \inferrule \mpr@infer |
nipkow@15337 | 338 |
|
nipkow@15337 | 339 |
% make a short name \infer is not already defined |
nipkow@15337 | 340 |
\@ifundefined {infer}{\let \infer \mpr@infer}{} |
nipkow@15337 | 341 |
|
nipkow@15337 | 342 |
\def \tir@name #1{\hbox {\small \sc #1}} |
nipkow@15337 | 343 |
\let \TirName \tir@name |
nipkow@15337 | 344 |
|
nipkow@15337 | 345 |
%%% Other Exports |
nipkow@15337 | 346 |
|
nipkow@15337 | 347 |
% \let \listcons \mpr@cons |
nipkow@15337 | 348 |
% \let \listsnoc \mpr@snoc |
nipkow@15337 | 349 |
% \let \listhead \mpr@head |
nipkow@15337 | 350 |
% \let \listmake \mpr@makelist |
nipkow@15337 | 351 |
|
nipkow@15337 | 352 |
|
nipkow@15337 | 353 |
\endinput |
nipkow@15337 | 354 |