https://github.com/EasyCrypt/easycrypt
Tip revision: a79f9aeb6de046ca12210d26317fab59c175d0dd authored by Pierre-Yves Strub on 08 July 2014, 09:43:21 UTC
Fix bug w.r.t. _tools presence detection.
Fix bug w.r.t. _tools presence detection.
Tip revision: a79f9ae
infer.sty
%\provide {rule}
%==========================================================================
%%%% PROOFS
%----------
%%% Judgements
\let\th=\vdash
%==========================================================================
%%% To produce a derivation separated by a line...
% The syntax is
%
% <command> { <hypothesis> <middle> <conclusion> } [<labeling>]
%
%%%
% Internal use
\let \midrule=\hrule
\def \openrule {\vbox \bgroup \halign \bgroup \hfil $##$\hfil \cr}
\def \closerule {\crcr\egroup\egroup}
\def \midclosure {\crcr\noalign {\vskip -0.1em}\closerule}
\let \labclosure = \midclosure
\def \middlerule {\midclosure\over\openrule}
\def \Midclosure {\crcr \noalign
{\vskip 0.3em \midrule \vskip -0.2em}\midclosure}
\def \Middlerule {\Midclosure\over\openrule}
\def \MIDCLOSURE {\crcr \noalign
{\vskip 0.3em \midrule \vskip 0.1em \midrule \vskip -0.2em}\midclosure}
\def \MIDDLERULE {\MIDCLOSURE\over\openrule}
% End internal use
%% <command> are...
\def \lessskip {\lineskiplimit=.3em\lineskip= .2em plus .1em}
\def \beginrule {\displaystyle \offinterlineskip \lessskip
\norulelab \bgroup \openrule}
\def \endrule {\closerule \egroup \rulelab}
\def \mathrule #1{\beginrule #1\endrule}
\def\infrule#1#2{\displaystyle \offinterlineskip \lessskip
\norulelab
\frac{\openrule#1\midclosure}{\openrule#2\closerule}
\rulelab}
%% <middle> is
\let \mir \middlerule
\let \Mir \Middlerule
\let \MIR \MIDDLERULE
\def \setdoublerule {\let \mir \Middlerule \let \labclosure \Midclosure}
\def \settripplerule {\let \mir \MIDDLERULE \let \labclosure \MIDCLOSURE}
\let \nl \mir
\let \NL \MIR
% Internal or personal use
\def \gluelab{\hskip .5em}
\def \namelab#1{{\rm(\name{#1})}}
\def \namelabb#1{{\rm\name{#1}}}
\let \lab = \namelab
\let \labb = \namelabb
% End of internal use
%% <Labelling> is...
%
% <option> anything but an opening bracket [ <label> ]
%
% or
%
% <nolab>
%
% where <option> is one of the fourth
\def \rl {\gluelab \lab}
\def \rlb {\gluelab \labb}
\def \lll #1{\lab {#1}\gluelab}
\def \Rl #1{\rlap {\rl{#1}}}
\def \lll #1{\llap {\lll{#1}}}
\def \norulelab {\let \rulelab \relax}
\def \labrule #1{\labclosure \over \gdef \rulelab {#1}\openrule}
\def \rlab #1[#2]{\labrule {\rl {#2}}}
\def \Rlab #1[#2]{\labrule {\lll {#2}}}
\def \llab #1[#2]{\labrule {\Rl {#1}}}
\def \Llab #1[#2]{\labrule {\Ll {#2}}}
% ... to put the label on the left or right of the rule
% In Capitalized commands, labels will not influence the length of the line
% A good separator for multiple hypothesis
% \qquad on the same line
% \andcr carriage return
\let \andcr \cr
% By default the rule is '-------', but it can be turn into '======'
% by executing \setdoublerule before typing the rule. Gouping could
% be needed to prevent this side effect from escaping.
\expandafter\ifx\csname name\endcsname\relax
\def\name#1{\hbox{\sc #1}}\else \relax \fi
\def \Mathrule #1{\beginMathrule#1\endMathrule}
\def \beginMathrule #1\nl #2\endMathrule
{\newdimen\Ruledimen \newdimen\ruledimen
\setbox0=\hbox {$\displaystyle \openrule#1\closerule$}\ruledimen=\wd0
\setbox0=\hbox {$\displaystyle \openrule#2\closerule$}\Ruledimen=\wd0
\ifnum \wd0>\ruledimen
\advance \Ruledimen by -\ruledimen
\divide \Ruledimen by 2
\else
\Ruledimen=0em
\fi
\def \midrule
{\vskip-0.2em
\hbox to \ruledimen
{\hskip-\Ruledimen\hrulefill\hskip -\Ruledimen}}
\beginrule #1\MIR#2\endrule}