Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
I
iris-coq
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Build
Pipelines
Jobs
Pipeline schedules
Artifacts
Deploy
Releases
Model registry
Operate
Environments
Monitor
Incidents
Service Desk
Analyze
Value stream analytics
Contributor analytics
CI/CD analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Terms and privacy
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
Dan Frumin
iris-coq
Commits
f8078dc2
Commit
f8078dc2
authored
8 years ago
by
Ralf Jung
Browse files
Options
Downloads
Patches
Plain Diff
mathpartir is in TexLive. remove it.
parent
e5973e6f
No related branches found
No related tags found
No related merge requests found
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
docs/mathpartir.sty
+0
-446
0 additions, 446 deletions
docs/mathpartir.sty
with
0 additions
and
446 deletions
docs/mathpartir.sty
deleted
100644 → 0
+
0
−
446
View file @
e5973e6f
% Mathpartir --- Math Paragraph for Typesetting Inference Rules
%
% Copyright (C) 2001, 2002, 2003, 2004, 2005 Didier Rmy
%
% Author : Didier Remy
% Version : 1.2.0
% Bug Reports : to author
% Web Site : http://pauillac.inria.fr/~remy/latex/
%
% 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, 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
% (http://pauillac.inria.fr/~remy/license/GPL).
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% File mathpartir.sty (LaTeX macros)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\NeedsTeXFormat
{
LaTeX2e
}
\ProvidesPackage
{
mathpartir
}
[2005/12/20 version 1.2.0 Math Paragraph for Typesetting Inference Rules]
%%
%% Identification
%% Preliminary declarations
\RequirePackage
{
keyval
}
%% Options
%% 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
% To ensure hevea \hva compatibility, \hva should expands to nothing
% in mathpar or in inferrule
\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
@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
}
\let
\MathparBindings
\mpr
@bindings
% \@ifundefined {ignorespacesafterend}
% {\def \ignorespacesafterend {\aftergroup \ignorespaces}
\newenvironment
{
mathpar
}
[1][]
{$$
\mpr
@savepar
\parskip
0
em
\hsize
\linewidth
\centering
\vbox
\bgroup
\mpr
@prebindings
\mpr
@paroptions #
1
\ifmmode
$
\else
\noindent
$
\displaystyle\fi
\MathparBindings
}
{
\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
}
% \def \math@mathpar #1{\setbox0 \hbox {$\displaystyle #1$}\ifnum
% \wd0 < \hsize $$\box0$$\else \bmathpar #1\emathpar \fi}
%%% 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
{
\setbox
0
\hbox
{
\let
\\\qquad
$
#
1
$}
\ifnum
\wd
0 <
\hsize
\box
0
\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
\if
@premisse
\newbox
\mpr
@hlist
\newbox
\mpr
@vlist
\newif
\ifmpr
@center
\mpr
@centertrue
\def
\mpr
@htovlist
{
%
\setbox
\mpr
@hlist
\hbox
{
\strut
\ifmpr
@center
\hskip
-0.5
\wd\mpr
@hlist
\fi
\unhbox
\mpr
@hlist
}
%
\setbox
\mpr
@vlist
\vbox
{
\if
@premisse
\box
\mpr
@hlist
\unvbox
\mpr
@vlist
\else
\unvbox
\mpr
@vlist
\box
\mpr
@hlist
\fi
}
%
}
% OLD version
% \def \mpr@htovlist {%
% \setbox \mpr@hlist
% \hbox {\strut \hskip -0.5\wd\mpr@hlist \unhbox \mpr@hlist}%
% \setbox \mpr@vlist
% \vbox {\if@premisse \box \mpr@hlist \unvbox \mpr@vlist
% \else \unvbox \mpr@vlist \box \mpr@hlist
% \fi}%
% }
\def
\mpr
@item #1
{$
\displaystyle
#
1
$}
\def
\mpr
@sep
{
2em
}
\def
\mpr
@blank
{
}
\def
\mpr
@hovbox #1#2
{
\hbox
\bgroup
\ifx
#1T
\@
premissetrue
\else
\ifx
#1B
\@
premissefalse
\else
\PackageError
{
mathpartir
}
{
Premisse orientation should either be T or B
}
{
Fatal error in Package
}
%
\fi
\fi
\def
\@
test
{
#2
}
\ifx
\@
test
\mpr
@blank
\else
\setbox
\mpr
@hlist
\hbox
{}
%
\setbox
\mpr
@vlist
\vbox
{}
%
\if
@premisse
\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
\if
@premisse
\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
\setbox
0
\hbox
{
\mpr
@item
{
##1
}}
\relax
\advance
\mpr
@tmpdim by
\wd
0
%\mpr@tmpdim 1.02\mpr@tmpdim
\ifnum
\mpr
@tmpdim <
\hsize
\ifnum
\wd\mpr
@hlist > 0
\if
@premisse
\setbox
\mpr
@hlist
\hbox
{
\unhbox
0
\hskip
\mpr
@sep
\unhbox
\mpr
@hlist
}
%
\else
\setbox
\mpr
@hlist
\hbox
{
\unhbox
\mpr
@hlist
\hskip
\mpr
@sep
\unhbox
0
}
%
\fi
\else
\setbox
\mpr
@hlist
\hbox
{
\unhbox
0
}
%
\fi
\else
\ifnum
\wd
\mpr
@hlist > 0
\mpr
@htovlist
\mpr
@tmpdim
\wd
0
\fi
\setbox
\mpr
@hlist
\hbox
{
\unhbox
0
}
%
\fi
\advance
\mpr
@tmpdim by
\mpr
@sep
\fi
}
%
\@
rev
\mpr
@htovlist
\ifmpr
@center
\hskip
\wd\mpr
@vlist
\fi
\box
\mpr
@vlist
\fi
\egroup
}
%%% 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
@make@fraction #1#2#3#4#5
{
\hbox
{
%
\def
\mpr
@tail
{
#1
}
%
\def
\mpr
@body
{
#2
}
%
\def
\mpr
@head
{
#3
}
%
\setbox
1=
\hbox
{$
#
4
$}
\setbox
2=
\hbox
{$
#
5
$}
%
\setbox
3=
\hbox
{$
\mkern
-
3
mu
\mpr
@body
\mkern
-
3
mu
$}
%
\setbox
3=
\hbox
{$
\mkern
-
3
mu
\mpr
@body
\mkern
-
3
mu
$}
%
\dimen
0=
\dp
1
\advance\dimen
0 by
\ht
3
\relax\dp
1
\dimen
0
\relax
\dimen
0=
\ht
2
\advance\dimen
0 by
\dp
3
\relax\ht
2
\dimen
0
\relax
\setbox
0=
\hbox
{$
\box
1
\@
@atop
\box
2
$}
%
\dimen
0=
\wd
0
\box
0
\box
0
\hskip
-
\dimen
0
\relax
\hbox
to
\dimen
0
{$
%
\mathrel
{
\mpr
@tail
}
\joinrel
\xleaders\hbox
{
\copy
3
}
\hfil\joinrel\mathrel
{
\mpr
@head
}
%
$}}}
%% Old stuff should be removed in next version
\def
\mpr
@@nothing #1#2
{$
\lower
0
.
01
pt
\mpr
@@nofraction
{
#
1
}{
#
2
}$}
\def
\mpr
@@reduce #1#2
{
\hbox
{$
\lower
0
.
01
pt
\mpr
@@fraction
{
#
1
}{
#
2
}
\mkern
-
15
mu
\rightarrow
$}}
\def
\mpr
@@rewrite #1#2#3
{
\hbox
{$
\lower
0
.
01
pt
\mpr
@@fraction
{
#
2
}{
#
3
}
\mkern
-
8
mu#
1
$}}
\def
\mpr
@infercenter #1
{
\vcenter
{
\mpr
@hovbox
{
T
}{
#1
}}}
\def
\mpr
@empty
{}
\def
\mpr
@inferrule
{
\bgroup
\ifnum
\linewidth
<
\hsize
\hsize
\linewidth\fi
\mpr
@rulelineskip
\let
\and
\qquad
\let
\hva
\mpr
@hva
\let
\@
rulename
\mpr
@empty
\let
\@
rule@options
\mpr
@empty
\let
\mpr
@over
\@
@over
\mpr
@inferrule@
}
\newcommand
{
\mpr
@inferrule@
}
[3][]
{
\everymath
=
{
\displaystyle
}
%
\def
\@
test
{
#2
}
\ifx
\empty
\@
test
\setbox
0
\hbox
{$
\vcenter
{
\mpr
@hovbox
{
B
}{
#
3
}}$}
%
\else
\def
\@
test
{
#3
}
\ifx
\empty
\@
test
\setbox
0
\hbox
{$
\vcenter
{
\mpr
@hovbox
{
T
}{
#
2
}}$}
%
\else
\setbox
0
\mpr
@fraction
{
\mpr
@hovbox
{
T
}{
#2
}}{
\mpr
@hovbox
{
B
}{
#3
}}
%
\fi
\fi
\def
\@
test
{
#1
}
\ifx
\@
test
\empty
\box
0
\else
\vbox
%%% Suggestion de Francois pour les etiquettes longues
%%% {\hbox to \wd0 {\RefTirName {#1}\hfil}\box0}\fi
{
\hbox
{
\RefTirName
{
#1
}}
\box
0
}
\fi
\egroup
}
\def
\mpr
@vdotfil #1
{
\vbox
to #1
{
\leaders
\hbox
{$
\cdot
$}
\vfil
}}
% They are two forms
% \inferrule [label]{[premisses}{conclusions}
% or
% \inferrule* [options]{[premisses}{conclusions}
%
% Premisses and conclusions are lists of elements separated by \\
% Each \\ produces a break, attempting horizontal breaks if possible,
% and vertical breaks if needed.
%
% An empty element obtained by \\\\ produces a vertical break in all cases.
%
% The former rule is aligned on the fraction bar.
% The optional label appears on top of the rule
% The second form to be used in a derivation tree is aligned on the last
% line of its conclusion
%
% The second form can be parameterized, using the key=val interface. The
% folloiwng keys are recognized:
%
% width set the width of the rule to val
% narrower set the width of the rule to val\hsize
% before execute val at the beginning/left
% lab put a label [Val] on top of the rule
% lskip add negative skip on the right
% left put a left label [Val]
% Left put a left label [Val], ignoring its width
% right put a right label [Val]
% Right put a right label [Val], ignoring its width
% leftskip skip negative space on the left-hand side
% rightskip skip negative space on the right-hand side
% vdots lift the rule by val and fill vertical space with dots
% after execute val at the end/right
%
% Note that most options must come in this order to avoid strange
% typesetting (in particular leftskip must preceed left and Left and
% rightskip must follow Right or right; vdots must come last
% or be only followed by rightskip.
%
%% 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
}{
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
}{
sep
}{
\def\mpr
@sep
{
#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
}{
left
}{
\setbox
0
\hbox
{$
\TirName
{
#
1
}
\;
$}
\relax
\advance
\hsize
by -
\wd
0
\box
0
}
\define
@key
{
mpr
}{
width
}{
\hsize
#1
}
\define
@key
{
mpr
}{
sep
}{
\def\mpr
@sep
{
#1
}}
\define
@key
{
mpr
}{
before
}{
#1
}
\define
@key
{
mpr
}{
lab
}{
\let
\RefTirName
\TirName
\def
\mpr
@rulename
{
#1
}}
\define
@key
{
mpr
}{
Lab
}{
\let
\RefTirName
\TirName
\def
\mpr
@rulename
{
#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
{
mpr
}{
rightskip
}
{
\setbox
\mpr
@right
\hbox
{
\unhbox
\mpr
@right
\hskip
-#1
}}
\define
@key
{
mpr
}{
LEFT
}{
\setbox
0
\hbox
{$
#
1
$}
\relax
\advance
\hsize
by -
\wd
0
\box
0
}
\define
@key
{
mpr
}{
left
}{
\setbox
0
\hbox
{$
\TirName
{
#
1
}
\;
$}
\relax
\advance
\hsize
by -
\wd
0
\box
0
}
\define
@key
{
mpr
}{
Left
}{
\llap
{$
\TirName
{
#
1
}
\;
$}}
\define
@key
{
mpr
}{
right
}
{
\setbox
0
\hbox
{$
\;\TirName
{
#
1
}$}
\relax
\advance
\hsize
by -
\wd
0
\setbox
\mpr
@right
\hbox
{
\unhbox
\mpr
@right
\unhbox
0
}}
\define
@key
{
mpr
}{
RIGHT
}
{
\setbox
0
\hbox
{$
#
1
$}
\relax
\advance
\hsize
by -
\wd
0
\setbox
\mpr
@right
\hbox
{
\unhbox
\mpr
@right
\unhbox
0
}}
\define
@key
{
mpr
}{
Right
}
{
\setbox
\mpr
@right
\hbox
{
\unhbox
\mpr
@right
\rlap
{$
\;\TirName
{
#
1
}$}}}
\define
@key
{
mpr
}{
vdots
}{
\def
\mpr
@vdots
{
\@
@atop
\mpr
@vdotfil
{
#1
}}}
\define
@key
{
mpr
}{
after
}{
\edef
\mpr
@after
{
\mpr
@after #1
}}
\newcommand
\mpr
@inferstar@ [3][]
{
\setbox
0
\hbox
{
\let
\mpr
@rulename
\mpr
@empty
\let
\mpr
@vdots
\relax
\setbox
\mpr
@right
\hbox
{}
%
$
\setkeys
{
mpr
}{
#
1
}
%
\ifx
\mpr
@rulename
\mpr
@empty
\mpr
@inferrule
{
#
2
}{
#
3
}
\else
\mpr
@inferrule
[
{
\mpr
@rulename
}
]
{
#
2
}{
#
3
}
\fi
\box
\mpr
@right
\mpr
@vdots
$}
\setbox
1
\hbox
{
\strut
}
\@
tempdima
\dp
0
\advance
\@
tempdima by -
\dp
1
\raise
\@
tempdima
\box
0
}
\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
% Envirnonment mathpar
\let
\inferrule
\mpr
@infer
% make a short name \infer is not already defined
\@
ifundefined
{
infer
}{
\let
\infer
\mpr
@infer
}{}
\def
\TirNameStyle
#1
{
\small
\textsc
{
#1
}}
\def
\tir
@name #1
{
\hbox
{
\small
\TirNameStyle
{
#1
}}}
\let
\TirName
\tir
@name
\let
\DefTirName
\TirName
\let
\RefTirName
\TirName
%%% Other Exports
% \let \listcons \mpr@cons
% \let \listsnoc \mpr@snoc
% \let \listhead \mpr@head
% \let \listmake \mpr@makelist
\endinput
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment