slides/mathpartir.sty
changeset 379 11f5f86bf956
parent 378 94988aa97974
child 380 948f4b39d55d
equal deleted inserted replaced
378:94988aa97974 379:11f5f86bf956
     1 %  Mathpartir --- Math Paragraph for Typesetting Inference Rules
       
     2 %
       
     3 %  Copyright (C) 2001, 2002, 2003, 2004, 2005 Didier Rémy
       
     4 %
       
     5 %  Author         : Didier Remy 
       
     6 %  Version        : 1.2.0
       
     7 %  Bug Reports    : to author
       
     8 %  Web Site       : http://pauillac.inria.fr/~remy/latex/
       
     9 % 
       
    10 %  Mathpartir is free software; you can redistribute it and/or modify
       
    11 %  it under the terms of the GNU General Public License as published by
       
    12 %  the Free Software Foundation; either version 2, or (at your option)
       
    13 %  any later version.
       
    14 %  
       
    15 %  Mathpartir is distributed in the hope that it will be useful,
       
    16 %  but WITHOUT ANY WARRANTY; without even the implied warranty of
       
    17 %  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
       
    18 %  GNU General Public License for more details 
       
    19 %  (http://pauillac.inria.fr/~remy/license/GPL).
       
    20 %
       
    21 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
    22 %  File mathpartir.sty (LaTeX macros)
       
    23 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
    24 
       
    25 \NeedsTeXFormat{LaTeX2e}
       
    26 \ProvidesPackage{mathpartir}
       
    27     [2005/12/20 version 1.2.0 Math Paragraph for Typesetting Inference Rules]
       
    28 
       
    29 %%
       
    30 
       
    31 %% Identification
       
    32 %% Preliminary declarations
       
    33 
       
    34 \RequirePackage {keyval}
       
    35 
       
    36 %% Options
       
    37 %% More declarations
       
    38 
       
    39 %% PART I: Typesetting maths in paragraphe mode
       
    40 
       
    41 %% \newdimen \mpr@tmpdim
       
    42 %% Dimens are a precious ressource. Uses seems to be local.
       
    43 \let \mpr@tmpdim \@tempdima
       
    44 
       
    45 % To ensure hevea \hva compatibility, \hva should expands to nothing 
       
    46 % in mathpar or in inferrule
       
    47 \let \mpr@hva \empty
       
    48 
       
    49 %% normal paragraph parametters, should rather be taken dynamically
       
    50 \def \mpr@savepar {%
       
    51   \edef \MathparNormalpar
       
    52      {\noexpand \lineskiplimit \the\lineskiplimit
       
    53       \noexpand \lineskip \the\lineskip}%
       
    54   }
       
    55 
       
    56 \def \mpr@rulelineskip {\lineskiplimit=0.3em\lineskip=0.2em plus 0.1em}
       
    57 \def \mpr@lesslineskip {\lineskiplimit=0.6em\lineskip=0.5em plus 0.2em}
       
    58 \def \mpr@lineskip  {\lineskiplimit=1.2em\lineskip=1.2em plus 0.2em}
       
    59 \let \MathparLineskip \mpr@lineskip
       
    60 \def \mpr@paroptions {\MathparLineskip}
       
    61 \let \mpr@prebindings \relax
       
    62 
       
    63 \newskip \mpr@andskip \mpr@andskip 2em plus 0.5fil minus 0.5em
       
    64 
       
    65 \def \mpr@goodbreakand
       
    66    {\hskip -\mpr@andskip  \penalty -1000\hskip \mpr@andskip}
       
    67 \def \mpr@and {\hskip \mpr@andskip}
       
    68 \def \mpr@andcr {\penalty 50\mpr@and}
       
    69 \def \mpr@cr {\penalty -10000\mpr@and}
       
    70 \def \mpr@eqno #1{\mpr@andcr #1\hskip 0em plus -1fil \penalty 10}
       
    71 
       
    72 \def \mpr@bindings {%
       
    73   \let \and \mpr@andcr
       
    74   \let \par \mpr@andcr
       
    75   \let \\\mpr@cr
       
    76   \let \eqno \mpr@eqno
       
    77   \let \hva \mpr@hva
       
    78   } 
       
    79 \let \MathparBindings \mpr@bindings
       
    80 
       
    81 % \@ifundefined {ignorespacesafterend}
       
    82 %    {\def \ignorespacesafterend {\aftergroup \ignorespaces}
       
    83 
       
    84 \newenvironment{mathpar}[1][]
       
    85   {$$\mpr@savepar \parskip 0em \hsize \linewidth \centering
       
    86      \vbox \bgroup \mpr@prebindings \mpr@paroptions #1\ifmmode $\else
       
    87      \noindent $\displaystyle\fi
       
    88      \MathparBindings}
       
    89   {\unskip \ifmmode $\fi\egroup $$\ignorespacesafterend}
       
    90 
       
    91 \newenvironment{mathparpagebreakable}[1][]
       
    92   {\begingroup 
       
    93    \par
       
    94    \mpr@savepar \parskip 0em \hsize \linewidth \centering
       
    95       \mpr@prebindings \mpr@paroptions #1%
       
    96       \vskip \abovedisplayskip \vskip -\lineskip%
       
    97      \ifmmode  \else  $\displaystyle\fi
       
    98      \MathparBindings
       
    99   }
       
   100   {\unskip
       
   101    \ifmmode $\fi \par\endgroup
       
   102    \vskip \belowdisplayskip
       
   103    \noindent
       
   104   \ignorespacesafterend}
       
   105 
       
   106 % \def \math@mathpar #1{\setbox0 \hbox {$\displaystyle #1$}\ifnum
       
   107 %     \wd0 < \hsize  $$\box0$$\else \bmathpar #1\emathpar \fi}
       
   108 
       
   109 %%% HOV BOXES
       
   110 
       
   111 \def \mathvbox@ #1{\hbox \bgroup \mpr@normallineskip 
       
   112   \vbox \bgroup \tabskip 0em \let \\ \cr
       
   113   \halign \bgroup \hfil $##$\hfil\cr #1\crcr \egroup \egroup
       
   114   \egroup}
       
   115 
       
   116 \def \mathhvbox@ #1{\setbox0 \hbox {\let \\\qquad $#1$}\ifnum \wd0 < \hsize
       
   117       \box0\else \mathvbox {#1}\fi}
       
   118 
       
   119 
       
   120 %% Part II -- operations on lists
       
   121 
       
   122 \newtoks \mpr@lista
       
   123 \newtoks \mpr@listb
       
   124 
       
   125 \long \def\mpr@cons #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
       
   126 {#2}\edef #2{\the \mpr@lista \the \mpr@listb}}
       
   127 
       
   128 \long \def\mpr@snoc #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
       
   129 {#2}\edef #2{\the \mpr@listb\the\mpr@lista}}
       
   130 
       
   131 \long \def \mpr@concat#1=#2\mpr@to#3{\mpr@lista \expandafter {#2}\mpr@listb
       
   132 \expandafter {#3}\edef #1{\the \mpr@listb\the\mpr@lista}}
       
   133 
       
   134 \def \mpr@head #1\mpr@to #2{\expandafter \mpr@head@ #1\mpr@head@ #1#2}
       
   135 \long \def \mpr@head@ #1#2\mpr@head@ #3#4{\def #4{#1}\def#3{#2}}
       
   136 
       
   137 \def \mpr@flatten #1\mpr@to #2{\expandafter \mpr@flatten@ #1\mpr@flatten@ #1#2}
       
   138 \long \def \mpr@flatten@ \\#1\\#2\mpr@flatten@ #3#4{\def #4{#1}\def #3{\\#2}}
       
   139 
       
   140 \def \mpr@makelist #1\mpr@to #2{\def \mpr@all {#1}%
       
   141    \mpr@lista {\\}\mpr@listb \expandafter {\mpr@all}\edef \mpr@all {\the
       
   142    \mpr@lista \the \mpr@listb \the \mpr@lista}\let #2\empty 
       
   143    \def \mpr@stripof ##1##2\mpr@stripend{\def \mpr@stripped{##2}}\loop
       
   144      \mpr@flatten \mpr@all \mpr@to \mpr@one
       
   145      \expandafter \mpr@snoc \mpr@one \mpr@to #2\expandafter \mpr@stripof
       
   146      \mpr@all \mpr@stripend  
       
   147      \ifx \mpr@stripped \empty \let \mpr@isempty 0\else \let \mpr@isempty 1\fi
       
   148      \ifx 1\mpr@isempty
       
   149    \repeat
       
   150 }
       
   151 
       
   152 \def \mpr@rev #1\mpr@to #2{\let \mpr@tmp \empty
       
   153    \def \\##1{\mpr@cons ##1\mpr@to \mpr@tmp}#1\let #2\mpr@tmp}
       
   154 
       
   155 %% Part III -- Type inference rules
       
   156 
       
   157 \newif \if@premisse
       
   158 \newbox \mpr@hlist
       
   159 \newbox \mpr@vlist
       
   160 \newif \ifmpr@center \mpr@centertrue
       
   161 \def \mpr@htovlist {%
       
   162    \setbox \mpr@hlist
       
   163       \hbox {\strut
       
   164              \ifmpr@center \hskip -0.5\wd\mpr@hlist\fi
       
   165              \unhbox \mpr@hlist}%
       
   166    \setbox \mpr@vlist
       
   167       \vbox {\if@premisse  \box \mpr@hlist \unvbox \mpr@vlist
       
   168              \else \unvbox \mpr@vlist \box \mpr@hlist
       
   169              \fi}%
       
   170 }
       
   171 % OLD version
       
   172 % \def \mpr@htovlist {%
       
   173 %    \setbox \mpr@hlist
       
   174 %       \hbox {\strut \hskip -0.5\wd\mpr@hlist \unhbox \mpr@hlist}%
       
   175 %    \setbox \mpr@vlist
       
   176 %       \vbox {\if@premisse  \box \mpr@hlist \unvbox \mpr@vlist
       
   177 %              \else \unvbox \mpr@vlist \box \mpr@hlist
       
   178 %              \fi}%
       
   179 % }
       
   180 
       
   181 \def \mpr@item #1{$\displaystyle #1$}
       
   182 \def \mpr@sep{2em}
       
   183 \def \mpr@blank { }
       
   184 \def \mpr@hovbox #1#2{\hbox
       
   185   \bgroup
       
   186   \ifx #1T\@premissetrue
       
   187   \else \ifx #1B\@premissefalse
       
   188   \else
       
   189      \PackageError{mathpartir}
       
   190        {Premisse orientation should either be T or B}
       
   191        {Fatal error in Package}%
       
   192   \fi \fi
       
   193   \def \@test {#2}\ifx \@test \mpr@blank\else
       
   194   \setbox \mpr@hlist \hbox {}%
       
   195   \setbox \mpr@vlist \vbox {}%
       
   196   \if@premisse \let \snoc \mpr@cons \else \let \snoc \mpr@snoc \fi
       
   197   \let \@hvlist \empty \let \@rev \empty
       
   198   \mpr@tmpdim 0em
       
   199   \expandafter \mpr@makelist #2\mpr@to \mpr@flat
       
   200   \if@premisse \mpr@rev \mpr@flat \mpr@to \@rev \else \let \@rev \mpr@flat \fi
       
   201   \def \\##1{%
       
   202      \def \@test {##1}\ifx \@test \empty
       
   203         \mpr@htovlist
       
   204         \mpr@tmpdim 0em %%% last bug fix not extensively checked
       
   205      \else
       
   206       \setbox0 \hbox{\mpr@item {##1}}\relax
       
   207       \advance \mpr@tmpdim by \wd0
       
   208       %\mpr@tmpdim 1.02\mpr@tmpdim
       
   209       \ifnum \mpr@tmpdim < \hsize
       
   210          \ifnum \wd\mpr@hlist > 0
       
   211            \if@premisse
       
   212              \setbox \mpr@hlist 
       
   213                 \hbox {\unhbox0 \hskip \mpr@sep \unhbox \mpr@hlist}%
       
   214            \else
       
   215              \setbox \mpr@hlist
       
   216                 \hbox {\unhbox \mpr@hlist  \hskip \mpr@sep \unhbox0}%
       
   217            \fi
       
   218          \else 
       
   219          \setbox \mpr@hlist \hbox {\unhbox0}%
       
   220          \fi
       
   221       \else
       
   222          \ifnum \wd \mpr@hlist > 0
       
   223             \mpr@htovlist 
       
   224             \mpr@tmpdim \wd0
       
   225          \fi
       
   226          \setbox \mpr@hlist \hbox {\unhbox0}%
       
   227       \fi
       
   228       \advance \mpr@tmpdim by \mpr@sep
       
   229    \fi
       
   230    }%
       
   231    \@rev
       
   232    \mpr@htovlist
       
   233    \ifmpr@center \hskip \wd\mpr@vlist\fi \box \mpr@vlist
       
   234    \fi
       
   235    \egroup
       
   236 }
       
   237 
       
   238 %%% INFERENCE RULES
       
   239 
       
   240 \@ifundefined{@@over}{%
       
   241     \let\@@over\over % fallback if amsmath is not loaded
       
   242     \let\@@overwithdelims\overwithdelims
       
   243     \let\@@atop\atop \let\@@atopwithdelims\atopwithdelims
       
   244     \let\@@above\above \let\@@abovewithdelims\abovewithdelims
       
   245   }{}
       
   246 
       
   247 %% The default
       
   248 
       
   249 \def \mpr@@fraction #1#2{\hbox {\advance \hsize by -0.5em
       
   250     $\displaystyle {#1\mpr@over #2}$}}
       
   251 \def \mpr@@nofraction #1#2{\hbox {\advance \hsize by -0.5em
       
   252     $\displaystyle {#1\@@atop #2}$}}
       
   253 
       
   254 \let \mpr@fraction \mpr@@fraction
       
   255 
       
   256 %% A generic solution to arrow
       
   257 
       
   258 \def \mpr@make@fraction #1#2#3#4#5{\hbox {%
       
   259      \def \mpr@tail{#1}%
       
   260      \def \mpr@body{#2}%
       
   261      \def \mpr@head{#3}%
       
   262      \setbox1=\hbox{$#4$}\setbox2=\hbox{$#5$}%
       
   263      \setbox3=\hbox{$\mkern -3mu\mpr@body\mkern -3mu$}%
       
   264      \setbox3=\hbox{$\mkern -3mu \mpr@body\mkern -3mu$}%
       
   265      \dimen0=\dp1\advance\dimen0 by \ht3\relax\dp1\dimen0\relax
       
   266      \dimen0=\ht2\advance\dimen0 by \dp3\relax\ht2\dimen0\relax
       
   267      \setbox0=\hbox {$\box1 \@@atop \box2$}%
       
   268      \dimen0=\wd0\box0
       
   269      \box0 \hskip -\dimen0\relax
       
   270      \hbox to \dimen0 {$%
       
   271        \mathrel{\mpr@tail}\joinrel
       
   272        \xleaders\hbox{\copy3}\hfil\joinrel\mathrel{\mpr@head}%
       
   273      $}}}
       
   274 
       
   275 %% Old stuff should be removed in next version
       
   276 \def \mpr@@nothing #1#2
       
   277     {$\lower 0.01pt \mpr@@nofraction {#1}{#2}$}
       
   278 \def \mpr@@reduce #1#2{\hbox
       
   279     {$\lower 0.01pt \mpr@@fraction {#1}{#2}\mkern -15mu\rightarrow$}}
       
   280 \def \mpr@@rewrite #1#2#3{\hbox
       
   281     {$\lower 0.01pt \mpr@@fraction {#2}{#3}\mkern -8mu#1$}}
       
   282 \def \mpr@infercenter #1{\vcenter {\mpr@hovbox{T}{#1}}}
       
   283 
       
   284 \def \mpr@empty {}
       
   285 \def \mpr@inferrule
       
   286   {\bgroup
       
   287      \ifnum \linewidth<\hsize \hsize \linewidth\fi
       
   288      \mpr@rulelineskip
       
   289      \let \and \qquad
       
   290      \let \hva \mpr@hva
       
   291      \let \@rulename \mpr@empty
       
   292      \let \@rule@options \mpr@empty
       
   293      \let \mpr@over \@@over
       
   294      \mpr@inferrule@}
       
   295 \newcommand {\mpr@inferrule@}[3][]
       
   296   {\everymath={\displaystyle}%       
       
   297    \def \@test {#2}\ifx \empty \@test
       
   298       \setbox0 \hbox {$\vcenter {\mpr@hovbox{B}{#3}}$}%
       
   299    \else 
       
   300    \def \@test {#3}\ifx \empty \@test
       
   301       \setbox0 \hbox {$\vcenter {\mpr@hovbox{T}{#2}}$}%
       
   302    \else
       
   303    \setbox0 \mpr@fraction {\mpr@hovbox{T}{#2}}{\mpr@hovbox{B}{#3}}%
       
   304    \fi \fi
       
   305    \def \@test {#1}\ifx \@test\empty \box0
       
   306    \else \vbox 
       
   307 %%% Suggestion de Francois pour les etiquettes longues
       
   308 %%%   {\hbox to \wd0 {\RefTirName {#1}\hfil}\box0}\fi
       
   309       {\hbox {\RefTirName {#1}}\box0}\fi
       
   310    \egroup}
       
   311 
       
   312 \def \mpr@vdotfil #1{\vbox to #1{\leaders \hbox{$\cdot$} \vfil}}
       
   313 
       
   314 % They are two forms
       
   315 % \inferrule [label]{[premisses}{conclusions}
       
   316 % or
       
   317 % \inferrule* [options]{[premisses}{conclusions}
       
   318 %
       
   319 % Premisses and conclusions are lists of elements separated by \\
       
   320 % Each \\ produces a break, attempting horizontal breaks if possible, 
       
   321 % and  vertical breaks if needed. 
       
   322 % 
       
   323 % An empty element obtained by \\\\ produces a vertical break in all cases. 
       
   324 %
       
   325 % The former rule is aligned on the fraction bar. 
       
   326 % The optional label appears on top of the rule
       
   327 % The second form to be used in a derivation tree is aligned on the last
       
   328 % line of its conclusion
       
   329 % 
       
   330 % The second form can be parameterized, using the key=val interface. The
       
   331 % folloiwng keys are recognized:
       
   332 %       
       
   333 %  width                set the width of the rule to val
       
   334 %  narrower             set the width of the rule to val\hsize
       
   335 %  before               execute val at the beginning/left
       
   336 %  lab                  put a label [Val] on top of the rule
       
   337 %  lskip                add negative skip on the right
       
   338 %  left                 put a left label [Val]
       
   339 %  Left                 put a left label [Val],  ignoring its width 
       
   340 %  right                put a right label [Val]
       
   341 %  Right                put a right label [Val], ignoring its width
       
   342 %  leftskip             skip negative space on the left-hand side
       
   343 %  rightskip            skip negative space on the right-hand side
       
   344 %  vdots                lift the rule by val and fill vertical space with dots
       
   345 %  after                execute val at the end/right
       
   346 %  
       
   347 %  Note that most options must come in this order to avoid strange
       
   348 %  typesetting (in particular  leftskip must preceed left and Left and
       
   349 %  rightskip must follow Right or right; vdots must come last 
       
   350 %  or be only followed by rightskip. 
       
   351 %  
       
   352 
       
   353 %% Keys that make sence in all kinds of rules
       
   354 \def \mprset #1{\setkeys{mprset}{#1}}
       
   355 \define@key {mprset}{andskip}[]{\mpr@andskip=#1}
       
   356 \define@key {mprset}{lineskip}[]{\lineskip=#1}
       
   357 \define@key {mprset}{flushleft}[]{\mpr@centerfalse}
       
   358 \define@key {mprset}{center}[]{\mpr@centertrue}
       
   359 \define@key {mprset}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite}
       
   360 \define@key {mprset}{atop}[]{\let \mpr@fraction \mpr@@nofraction}
       
   361 \define@key {mprset}{myfraction}[]{\let \mpr@fraction #1}
       
   362 \define@key {mprset}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}}
       
   363 \define@key {mprset}{sep}{\def\mpr@sep{#1}}
       
   364 
       
   365 \newbox \mpr@right
       
   366 \define@key {mpr}{flushleft}[]{\mpr@centerfalse}
       
   367 \define@key {mpr}{center}[]{\mpr@centertrue}
       
   368 \define@key {mpr}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite}
       
   369 \define@key {mpr}{myfraction}[]{\let \mpr@fraction #1}
       
   370 \define@key {mpr}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}}
       
   371 \define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
       
   372      \advance \hsize by -\wd0\box0}
       
   373 \define@key {mpr}{width}{\hsize #1}
       
   374 \define@key {mpr}{sep}{\def\mpr@sep{#1}}
       
   375 \define@key {mpr}{before}{#1}
       
   376 \define@key {mpr}{lab}{\let \RefTirName \TirName \def \mpr@rulename {#1}}
       
   377 \define@key {mpr}{Lab}{\let \RefTirName \TirName \def \mpr@rulename {#1}}
       
   378 \define@key {mpr}{narrower}{\hsize #1\hsize}
       
   379 \define@key {mpr}{leftskip}{\hskip -#1}
       
   380 \define@key {mpr}{reduce}[]{\let \mpr@fraction \mpr@@reduce}
       
   381 \define@key {mpr}{rightskip}
       
   382   {\setbox \mpr@right \hbox {\unhbox \mpr@right \hskip -#1}}
       
   383 \define@key {mpr}{LEFT}{\setbox0 \hbox {$#1$}\relax
       
   384      \advance \hsize by -\wd0\box0}
       
   385 \define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
       
   386      \advance \hsize by -\wd0\box0}
       
   387 \define@key {mpr}{Left}{\llap{$\TirName {#1}\;$}}
       
   388 \define@key {mpr}{right}
       
   389   {\setbox0 \hbox {$\;\TirName {#1}$}\relax \advance \hsize by -\wd0
       
   390    \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
       
   391 \define@key {mpr}{RIGHT}
       
   392   {\setbox0 \hbox {$#1$}\relax \advance \hsize by -\wd0
       
   393    \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
       
   394 \define@key {mpr}{Right}
       
   395   {\setbox \mpr@right \hbox {\unhbox \mpr@right \rlap {$\;\TirName {#1}$}}}
       
   396 \define@key {mpr}{vdots}{\def \mpr@vdots {\@@atop \mpr@vdotfil{#1}}}
       
   397 \define@key {mpr}{after}{\edef \mpr@after {\mpr@after #1}}
       
   398 
       
   399 \newcommand \mpr@inferstar@ [3][]{\setbox0
       
   400   \hbox {\let \mpr@rulename \mpr@empty \let \mpr@vdots \relax
       
   401          \setbox \mpr@right \hbox{}%
       
   402          $\setkeys{mpr}{#1}%
       
   403           \ifx \mpr@rulename \mpr@empty \mpr@inferrule {#2}{#3}\else
       
   404           \mpr@inferrule [{\mpr@rulename}]{#2}{#3}\fi
       
   405           \box \mpr@right \mpr@vdots$}
       
   406   \setbox1 \hbox {\strut}
       
   407   \@tempdima \dp0 \advance \@tempdima by -\dp1
       
   408   \raise \@tempdima \box0}
       
   409 
       
   410 \def \mpr@infer {\@ifnextchar *{\mpr@inferstar}{\mpr@inferrule}}
       
   411 \newcommand \mpr@err@skipargs[3][]{}
       
   412 \def \mpr@inferstar*{\ifmmode 
       
   413     \let \@do \mpr@inferstar@
       
   414   \else 
       
   415     \let \@do \mpr@err@skipargs
       
   416     \PackageError {mathpartir}
       
   417       {\string\inferrule* can only be used in math mode}{}%
       
   418   \fi \@do}
       
   419 
       
   420 
       
   421 %%% Exports
       
   422 
       
   423 % Envirnonment mathpar
       
   424 
       
   425 \let \inferrule \mpr@infer
       
   426 
       
   427 % make a short name \infer is not already defined
       
   428 \@ifundefined {infer}{\let \infer \mpr@infer}{}
       
   429 
       
   430 \def \TirNameStyle #1{\small \textsc{#1}}
       
   431 \def \tir@name #1{\hbox {\small \TirNameStyle{#1}}}
       
   432 \let \TirName \tir@name
       
   433 \let \DefTirName \TirName
       
   434 \let \RefTirName \TirName
       
   435 
       
   436 %%% Other Exports
       
   437 
       
   438 % \let \listcons \mpr@cons
       
   439 % \let \listsnoc \mpr@snoc
       
   440 % \let \listhead \mpr@head
       
   441 % \let \listmake \mpr@makelist
       
   442 
       
   443 
       
   444 
       
   445 
       
   446 \endinput