Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
% \iffalse meta-comment
%
% Copyright (C) 2011 by Jesse A. Tov
% ----------------------------------------------------
%
% This file may be distributed and/or modified under the
% conditions of the LaTeX Project Public License, either version 1.2
% of this license or (at your option) any later version.
% The latest version of this license is in:
%
% http://www.latex-project.org/lppl.txt
%
% and version 1.2 or later is part of all distributions of LaTeX
% version 1999/12/01 or later.
%
% ------------------------------------------------------------------
% This is a LaTeX package to make it easy to refer to nested labels
% using both an outer number (such as a theorem number) and an inner
% number (such as an item in an enumeration).
% ------------------------------------------------------------------
%
% *** The package file:
%\NeedsTeXFormat{LaTeX2e}[1999/12/01]
%\ProvidesPackage{pfsteps}
% [2011/04/04 v0.4 proof tools]
%
% *** The driver file:
%\NeedsTeXFormat{LaTeX2e}
%
% *** date, version, and stuff:
%\fi
%\ProvidesFile{pfsteps}
% [2011/04/04 v0.4 proof tools]
% \changes{v0.2}{2011/03/30}{Included listproc.sty}
% \changes{v0.1}{2011/03/26}{Initial documented release}
%
% \CheckSum{476}
% \CharacterTable
% {Upper-case \A\B\C\D\E\F\G\H\I\J\K\L\M\N\O\P\Q\R\S\T\U\V\W\X\Y\Z
% Lower-case \a\b\c\d\e\f\g\h\i\j\k\l\m\n\o\p\q\r\s\t\u\v\w\x\y\z
% Digits \0\1\2\3\4\5\6\7\8\9
% Exclamation \! Double quote \" Hash (number) \#
% Dollar \$ Percent \% Ampersand \&
% Acute accent \' Left paren \( Right paren \)
% Asterisk \* Plus \+ Comma \,
% Minus \- Point \. Solidus \/
% Colon \: Semicolon \; Less than \<
% Equals \= Greater than \> Question mark \?
% Commercial at \@ Left bracket \[ Backslash \\
% Right bracket \] Circumflex \^ Underscore \_
% Grave accent \` Left brace \{ Vertical bar \|
% Right brace \} Tilde \~}
%
% \iffalse
%
%<*driver>
\documentclass{ltxdoc}
\usepackage{pfsteps} \relax
\usepackage{hypdoc}
\EnableCrossrefs
\CodelineIndex
\RecordChanges
\begin{document}
\DocInput{pfsteps.dtx}
\end{document}
%
% \fi
%
% \GetFileInfo{pfsteps}
%
% \DoNotIndex{\newcommand,\newenvironment,\def,\relax,\do,\@gobble}
% \DoNotIndex{\if,\ifx,\else,\fi,\providecommand,\let,\global,\ignorespaces}
% \DoNotIndex{\@undefined,\expandafter,\@for,\@ifnextchar,\addtolength}
% \DoNotIndex{\aftergroup,\begin,\dp,\ht,\wd,\end,\ifdim}
% \DoNotIndex{\@firstoftwo,\@secondoftwo,\@notfound,\@tester}
% \DoNotIndex{\addtocounter,\advance,\edef,\empty,\gdef,\ifnum}
% \DoNotIndex{\long,\newcounter,\renewcommand,\setcounter,\the,\toksdef}
% \DoNotIndex{\value,\xdef,\\,\begingroup,\endgroup,\x,\a}
%
% {\catcode`\|=0 \catcode`\\=12
% |gdef|bslash{\}}
% \makeatletter\relax
%
% \newcommand{\usemacro}[2][altusage]{\relax
% \texttt{\bslash#2}\relax
% \indexmacro[#1]{#2}\relax
% }
% \newcommand{\seemacro}[2][altusage]{\relax
% \hyperlink{macro:#2}{\texttt{\bslash#2}}\relax
% \indexmacro[#1]{#2}\relax
% }
% \newcommand{\defmacro}[2][usage]{\relax
% \hypertarget{macro:#2}{\usemacro[#1]{#2}}\relax
% }
% \newcommand{\indexmacro}[2][altusage]{\relax
% \index{#2=\string\verb!*+\bslash#2+\string|#1}\relax\iffalse!\fi
% }
% \newcommand{\useenviron}[2][altusage]{\relax
% \texttt{#2}\relax
% \indexenviron[#1]{#2}\relax
% }
% \newcommand{\seeenviron}[2][altusage]{\relax
% \hyperlink{environ:#2}{\texttt{#2}}\relax
% \indexenviron[#1]{#2}\relax
% }
% \newcommand{\defenviron}[2][usage]{\relax
% \hypertarget{environ:#2}{\useenviron[#1]{#2}}\relax
% }
% \newcommand{\indexenviron}[2][altusage]{\relax
% \index{#2={\string\ttfamily\space#2} (environment)\string|#1}\relax
% \index{environments:>#2={\string\ttfamily\space#2}\string|#1}\relax
% }
% \newcommand{\useoption}[2][altusage]{\relax
% \texttt{#2}\relax
% \indexoption[#1]{#2}\relax
% }
% \newcommand{\seeoption}[2][altusage]{\relax
% \hyperlink{option:#2}{\texttt{#2}}\relax
% \indexoption[#1]{#2}\relax
% }
% \newcommand{\defoption}[2][usage]{\relax
% \hypertarget{option:#2}{\useoption[#1]{#2}}\relax
% }
% \newcommand{\indexoption}[2][altusage]{\relax
% \index{#2={\string\ttfamily\space#2} (package option)\string|#1}\relax
% \index{package options:>#2={\string\ttfamily\space#2}\string|#1}\relax
% }
% \newcommand{\useother}[2][altusage]{\relax
% \texttt{#2}\relax
% \indexother[#1]{#2}\relax
% }
% \newcommand{\seeother}[2][altusage]{\relax
% \hyperlink{other:#2}{\texttt{#2}}\relax
% \indexother[#1]{#2}\relax
% }
% \newcommand{\defother}[2][usage]{\relax
% \useother[#1]{#2}\relax
% }
% \newcommand{\indexother}[2][usage]{\relax
% \index{#2=\string\verb!*+#2+\string|#1}\relax\iffalse!\fi
% }
% \newcommand{\altusage}[1]{\emph{(#1)}}
%
% {
% \makeatletter
% \global\let\doc@old@tabular\tabular
% \global\def\doctabular{\begingroup\catcode`\|=12\relax\doc@tabular}
% \global\def\doc@tabular#1{\endgroup\doc@old@tabular{#1}}
% }
% \let\enddoctabular\endtabular
%
% \catcode`\|=12\relax
% \newenvironment{decl}[1][3ex]
% {\par\addvspace{#1}\noindent
% \begin{tabular}{|l|l|}\hline\ignorespaces}
% {\\\hline\end{tabular}\nopagebreak\par\addvspace{1ex}\noindent
% \aftergroup\ignorespaces}
% \catcode`\|=\active\relax
%
% \newcounter{macrosenv}
% \newenvironment{macros}[1]
% {\setcounter{macrosenv}{0}
% \@for\@each@macro:=#1\do{
% \addtocounter{macrosenv}{1}
% \expandafter\macro\expandafter{\csname\@each@macro\endcsname}
% }}
% {\@whilenum\value{macrosenv}>0\do{
% \addtocounter{macrosenv}{-1}
% \endmacro
% }}
%
% ^^A Setup for printing guillemets and bullets in \tt for code listings
% \newsavebox{\lguilbox}
% \newsavebox{\rguilbox}
% \newsavebox{\bulbox}
% \newlength{\lguillen}
% \newlength{\rguillen}
% \newlength{\bullen}
% \newlength{\ttcharlen}
%
% \sbox{\lguilbox}{\tt<}\setlength{\ttcharlen}{\wd\lguilbox}
%
% \sbox{\lguilbox}{\tt\tiny<}\setlength{\lguillen}{\wd\lguilbox}
% \def\ttlguil{\mbox{\raisebox{1.5pt}{^^A
% \kern0.5pt{\tt\tiny<}^^A
% \kern\ttcharlen\kern-2\lguillen\kern-1pt^^A
% {\tt\tiny<}\kern0.5pt}}}
%
% \sbox{\rguilbox}{\tt\tiny>}\setlength{\rguillen}{\wd\rguilbox}
% \def\ttrguil{\mbox{\raisebox{1.5pt}{^^A
% \kern0.5pt{\tt\tiny>}^^A
% \kern\ttcharlen\kern-2\rguillen\kern-1pt^^A
% {\tt\tiny>}\kern0.5pt}}}
%
% \def\ttbul{\raisebox{1.5pt}
% {\makebox[\ttcharlen]{\hfill{$\scriptscriptstyle\bullet$}\hfill}}}
%
% \title{The \textsf{pfsteps} package}
% \author{Jesse A. Tov \\ \texttt{tov@ccs.neu.edu}}
% \date{This document
% corresponds to \textsf{\filename}~\fileversion, dated \filedate.}
%
% \maketitle
%
% \tableofcontents
%
% \section{Introduction}
% \label{sec:intro}
%
% This package provides three distinct facilities for writing
% mathematical proofs: proof step labeling, proof sequences, and the
% |byCases| environment for case analysis.
%
% \paragraph{Proof step labeling.}
% The package provides a set of commands for numbering proof steps locally
% and referring back to those numbers.^^A
% \footnote{The idea is based on
% Didier R\'emy's \textsf{locallabel} package
% (\url{http://cristal.inria.fr/~remy/latex/}), but the execution is
% different. In \textsf{locallabel}, a proof step number is printed and
% labeled at the same time, whereas in this package, printing a proof
% step number merely sets the current label so that a subsequent
% \usemacro{pflabel} command can then attach a label to it. This is
% appropriate for writing other commands that generate proof step
% numbers automatically but don't always require the user to name them.
% Also, unlike \textsf{locallabel}, we store proof step labels between
% runs, so that forward references work.}
% For example, to get
% \begin{quote}
% \usepfcounter[socrates]~Socrates is a man, and
% \usepfcounter[men]~all men are mortal.
% Therefore, by \pfref{socrates,men}, Socrates is mortal.
% \end{quote}
% we might type:
% \begin{quote}
% \begin{verbatim}
% \usepfcounter[socrates]~Socrates is a man, and
% \usepfcounter[men]~all men are mortal.
% Therefore, by \pfref{socrates,men}, Socrates is mortal.\end{verbatim}
% \end{quote}
% The \usemacro{usepfcounter} command prints the next proof step
% number, and if given an optional argument, associates that label name
% with the proof step number. Alternatively, if we leave the optional
% argument out, we can capture the most recent proof step number using
% the \usemacro{pflabel} command. For example, for the first line above,
% we could have instead written:
% \begin{quote}
% \begin{verbatim}
% \usepfcounter~Socrates is a man\pflabel{socrates}, and\end{verbatim}
% \end{quote}
% We can then refer to proof step labels using the \usemacro{pfref}
% command, which takes a comma-separated list of proof step labels.
%
% Finally, the proof step labels are local. The command
% \usemacro{resetpfcounter} ends the current numbering run, starts
% at 1 again, and allows reusing the same labels as the previous
% numbering run. The package does not currently support refering to
% proof steps outside the current numbering run.
%
% \paragraph{Proof sequences.}
%
% We provide environment \useenviron{pfsteps} and \useenviron{pfsteps*}
% for line-by-line
% proofs with justifications.
% The |pfsteps| environment puts proof steps in math mode, and the
% |pfsteps*| environment puts steps in text mode.
% The lines are numbered using the proof
% step labeling commands described above. Combined together this
% supports interspersing proof steps with explanatory text.
% The |pfsteps|$[$|*|$]$ environments work like the |enumerate| list
% environment,
% except that their numbering uses proof labels, which can be named locally
% with \usemacro{pflabel}, and they defines a command \usemacro{BY}, which
% places proof step justifications to the right.
% For example, to get:
% \begin{quote}
% \setlength{\parskip}{0pt}
% \vspace{-1em}
% \resetpfcounter
% \begin{pfsteps*}
% \item Socrates is a man. \pflabel{socrates}
% \item All men are mortal. \pflabel{men}
% \end{pfsteps*}
% Therefore,
% \begin{pfsteps*}
% \item Socrates is mortal.
% \BY{\pfref{men,socrates}}
% \end{pfsteps*}
% \end{quote}
% we can type:
% \begin{quote}
% \begin{verbatim}
% \resetpfcounter
% \begin{pfsteps*}
% \item Socrates is a man. \pflabel{socrates}
% \item All men are mortal. \pflabel{men}
% \end{pfsteps*}
% Therefore,
% \begin{pfsteps*}
% \item Socrates is mortal.
% \BY{\pfref{men,socrates}}
% \end{pfsteps*}\end{verbatim}
% \end{quote}
%
% We also (optionally) define an abbreviated syntax, which looks like
% this:
%
% \begin{quote}
% |\pfstepstextmode| \\
% \ttlguil|@socrates Socrates is a man.| \\
% \ttbul|@men All men are mortal.|\ttrguil \\
% |Therefore,| \\
% \ttlguil|Socrates is mortal. \BY{\pfref{men,socrates}}|\ttrguil
% \end{quote}
%
% \paragraph{The \texttt{byCases} environment.}
%
% We provide the \useenviron{byCases} environment for proofs by cases.
% For example, to get this:
% \begin{quote}
% By cases on $n$:
% \begin{byCases}
% \case{0} Something.
% \case{n' + 1} Something else.
% \otherwise There is no otherwise!
% \end{byCases}
% \end{quote}
% type this:
% \begin{quote}
% \begin{verbatim}
% By cases on $n$:
% \begin{byCases}
% \case{0} Something.
% \case{n' + 1} Something else.
% \otherwise There is no otherwise!
% \end{byCases}\end{verbatim}
% \end{quote}
%
% \subsection{Requirements \& Other Packages}
%
% The \textsf{pfsteps} package depends on the \textsf{listproc} package,
% which is a non-standard \LaTeX{} package available at
% \url{http://www.ccs.neu.edu/~tov/code/latex/}.
%
% It cooperates with several other packages if they are loaded, and can
% load them by request:
% \begin{description}
% \item[\sf{hyperref}] If loaded, this package is used to
% create hyperlinks to proof steps from proof step references.
% \item[\sf{mathpartir}] If loaded, we define an \usemacro{icase}
% command
% within the \useenviron{byCases} environment
% for considering inference rules by
% cases. This non-standard package is available at
% \url{http://cristal.inria.fr/~remy/latex/}.
% \item[\normalfont{\sf ucs}, {\sf inputenc}]
% If these
% packages are loaded, we can use them to define a nice notation for
% writing sequence of proof steps. The \textsf{inputenc} package
% must be loaded with the |utf8x| option.
% \end{description}
%
% \section{Package Options}
%
% The package provides several options, which we document here.
%
% \newcommand{\optionbox}[2]{
% \addvspace{2ex}
% \par\noindent
% \begin{minipage}[t]{0.5\linewidth}
% \begin{decl}#1\end{decl}
% \end{minipage}{\emph{default:} #2}\par\noindent\ignorespaces
% }
%
% \optionbox{\defoption{atsign}, \defoption{noatsign}}{true}
% This option controls whether |@| may be used inside the
% \useenviron{pfsteps}$[$|*|$]$ environment as a shorthand for
% \usemacro{pflabel}. This is on by default, but supplying the
% |noatsign| option will turn it off.
%
% \optionbox{\defoption{hyperref}, \defoption{nohyperref}}{detect}
% This controls integration with the \textsf{hyperref} package. If
% neither option is specified, then we attempt to detect
% \textsf{hyperref} and use it if it's detected. Passing the
% |nohyperref| option will prevent this integration, even if
% \textsf{hyperref} is loaded. Passing the |hyperref| option will cause
% \textsf{hyperref} to be loaded if it wasn't already. Because
% \textsf{hyperref} likes to be loaded after other packages, it's
% probably best not to specify either of these options and load it
% yourself after other packages.
%
% \optionbox{\defoption{loadunicode}, \defoption{noloadunicode}}
% {state of \seeoption{unicode} option}
% This option has no effect unless the
% |unicode| option is turned on \emph{explicitly}, in which
% case it defaults to true as well. If
% this option is on, we load two packages:
% \begin{verbatim}
% \RequirePackage{ucs}
% \RequirePackage[utf8x]{inputenc}\end{verbatim}
% Turning this option off by supplying |noloadunicode| will prevent
% those packages from being loaded. (Note that if the |unicode| option
% is on, you probably need to load these or something like them in order
% for it to work, or even for \textsf{pfsteps} to load properly.)
%
% \optionbox{\defoption{mathpartir}, \defoption{nomathpartir}}{detect}
% As with the \seeoption{hyperref} option, this controls integration
% with another package---in this case, Didier R\'emy's
% \textsf{mathpartir}. We try to detect \textsf{mathpartir} by default,
% but specifying |nomathpartir| will prevent detection and integration,
% whereas explicitly passing the |mathpartir| option will cause it to be
% loaded.
%
% \optionbox{\defoption{unicode}, \defoption{nounicode}}{false}
% If this option is turned on, we define \ttlguil{} and \ttrguil{} as
% shorthand for the \useenviron{pfsteps} environment and \ttbul{} as
% |\item| within the environment. By default, enabling this option
% enables \seeoption{loadunicode} as well.
%
% Alternatively, it's possible to manually turn on the shorthand notation using
% different characters with \seemacro{pfstepsSetupUnicode}.
%
% \section{Command Reference}
%
% \subsection{Proof Step Labeling}
%
% \begin{decl}
% \defmacro{resetpfcounter} \oarg{proof-step}
% \end{decl}
% Reset the proof step counter to \meta{proof-step} (default 0), which
% starts a new proof section. Labels from before using this command
% become no longer accessible, but their names may be reused. By
% default, this is called by every \seemacro{case} command in the
% |byCases| environment, but it may be disabled by redefining
% \seemacro{byCasesEveryCase}.
%
% \begin{decl}
% \defmacro{usepfcounter} \oarg{label-name}
% \end{decl}
% Increment and print the proof counter. If \meta{label-name}
% is given, then we associate that name with the new proof step value.
% To change how the proof counter is formatted, redefine
% \seemacro{pfcounteranchor}.
%
% \begin{decl}
% \defmacro{pflabel} \marg{label-name}
% \end{decl}
% Associate \meta{label-name} with the current value of the proof
% step counter.
%
% \begin{decl}
% \defmacro{pfref}
% |{|\meta{label-name}$_1$|,|$\ldots$|,|\meta{label-name}$_k$|}|
% \end{decl}
% Print references to the proof steps associated with one or label
% names, which must be separated by commas. The proof step numbers are
% sorted, and then adjacent numbers are compressed into ranges.
%
% \begin{decl}
% \defmacro{steppfcounter} \oarg{label-name}
% \end{decl}
% Increment the proof counter, but don't print it. If \meta{label-name}
% is given, then we associate that name with the new proof step value.
%
% \begin{decl}
% \defmacro{thepfcounter} \\
% \hline
% \defmacro{thepfsectioncounter}
% \end{decl}
% These show the current proof counter and the proof section counter,
% respectively. (The proof section counter is incremented by each call
% to \usemacro{resetpfcounter}.
%
% \begin{decl}
% \defmacro{pfcounteranchor} \marg{proof-step} \\
% \hline
% \defmacro{pfcounterref} \marg{proof-step}
% \end{decl}
% These are used to format proof step anchors and references. By
% default, they just place parentheses around their arguments. Redefine
% them to change how proof step numbers appear.
%
% \subsection{Proof Sequences}
%
% \begin{decl}
% |\begin{|\defenviron{pfsteps}|}| \\
% | |\defmacro{item} \meta{math}
% $[$\defmacro{BY}\marg{justification}$]$ \\
% | |$\vdots$ \\
% |\end{pfsteps}|
% \end{decl}
% Make a list of numbered proof steps. Each |\item| is numbered using
% \seemacro{usepfcounter}, so several instances of the |pfsteps|
% environment in sequence will continue numbering from each to the next
% instead of starting each at 1. (To reset the numbering, use
% \seemacro{resetpfcounter}). Optionally, |\BY|\marg{justification}
% will print the provided justification for the given step in a
% column on the right.
%
% Within the extent of this environment, a macro \defmacro{AND} is
% defined, which prints the word ``and'' with appropriate space around
% it in math mode.
%
% \begin{decl}
% |\begin{|\defenviron{pfsteps*}|}| \\
% | |\defmacro{item} \meta{text}
% $[$\defmacro{BY}\marg{justification}$]$ \\
% | |$\vdots$ \\
% |\end{pfsteps*}|
% \end{decl}
% Like the |pfsteps| environment, but the proof steps are in text rather
% than math mode.
%
% \begin{decl}
% \defother{@}\meta{label-name}\verb*+ +
% \end{decl}
% Inside the |pfstep|$[$|*|$]$ environments, this is equivalent to
% \usemacro{pflabel}\marg{label-name}, unless option
% \seeoption{noatsign} is supplied, in which case |@| has no special
% meaning inside the proof step environments.
%
% \begin{decl}
% \defmacro{proofleftskip}|=|\meta{dimen} & \emph{default:} |2pc|
% \end{decl}
% This dimension parameter determines the space reserved to the left of
% each proof step for the step number.
%
% \begin{decl}
% \defmacro{proofrightwidth}|=|\meta{dimen} & \emph{default:}
% |0.3|\usemacro{linewidth}
% \end{decl}
% This dimension parameter determines the width used for proof step
% justifications printed in the right column by |\BY|.
%
% \subsubsection{Unicode Shorthand}
%
% If option \seeoption{unicode} is enabled, then this notation is
% defined:
% \begin{decl}
% \ttlguil \meta{math} $[$\defmacro{BY}\marg{justification}$]$\\
% \ttbul \meta{math} $[$\defmacro{BY}\marg{justification}$]$\\
% $\vdots$ \\
% \ttrguil
% \end{decl}
% This is equivalent to using the \useenviron{pfsteps} environment,
% where the first |\item| is started implicitly, and the Unicode bullet
% \ttbul\ starts subsequent items.
%
% \begin{decl}
% \defmacro{pfstepsmathmode} \\
% \hline
% \defmacro{pfstepstextmode}
% \end{decl}
% Toggle the meaning of \ttlguil\ldots\ttrguil\ between math mode
% (like environment |pfsteps|) and text mode (like environment
% |pfsteps*|). The initial state is math mode.
%
% \begin{decl}
% \defmacro{pfstepsSetupUnicode} \marg{start-code} \marg{stop-text}
% \marg{item-code}
% \end{decl}
% If option \seeoption{nounicode} is set, then this command may be used
% to customize the |pfsteps| environment shorthand notation to use other
% characters. The arguments are as follows:
% \begin{description}
% \item[\rm\meta{start-code}] The Unicode code point, in decimal, for
% starting the notation. When setup automatically using the |unicode|
% option, this is |171|, which is the code
% point for \ttlguil.
% \item[\rm\meta{stop-text}] The actual text for terminating the notation.
% When setup by the |unicode| option, this is \ttrguil.
% \item[\rm\meta{item-code}] The Unicode code point, in decimal, for the
% |\item| separator. When setup by the |unicode| option, this is
% |8226|, which is the code point for \ttbul.
% \end{description}
% Note that the first and third arguments are decimal numbers
% representing Unicode code points, whereas the second argument is the
% actual symbol or sequence of symbols to use.
%
% \subsection{The \texttt{byCases} Environment}
%
% \begin{decl}
% |\begin{|\defenviron{byCases}|}| \\
% | |\meta{by-cases-item} \ldots \\
% |\end{byCases}|
% \end{decl}
% Introduce a case analysis section. Its contents must be a sequence of
% items, which may be constructed out of several commands detailed
% below.
% This is similar to the
% \useenviron{description} environment, but it changes the behavior of
% |\item| and defines several other commands within its scope.
% These are the commands defined or affected by |byCases|:
% \begin{quotation}
% \begin{decl}[1ex]
% \defmacro{item} \oarg{math} \meta{text}
% \end{decl}
% Insert a case list item. If \meta{math} is supplied, then the
% ``bullet'' is ``\textbf{Case }|$|\meta{math}|$|\textbf{.}''
% If \meta{math} is not supplied,
% then we begin the item with ``\textbf{Otherwise.}''
% \begin{decl}
% \defmacro{case} \oarg{extra} \marg{math} \meta{text}
% \end{decl}
% Insert a case list item with ``\textbf{Case
% }|$|\meta{math}|$|\textbf.'
% Unlike |\item|,
% this always puts a line break before \meta{text}.
% To change the appearance or language, redefine
% \seemacro{byCasesCaseTemplate}.
%
% The optional argument \meta{extra} is some text to insert after the
% case head but before the line break. The default value is
% \seemacro{byCasesEveryCase}.
% \begin{decl}
% \defmacro{otherwise} \oarg{extra} \meta{text}
% \end{decl}
% Insert a case list item, with ``\textbf{Otherwise.}'' Unlike |\item|,
% this always puts a line break before \meta{text}.
% To change the appearance or language, redefine
% \seemacro{byCasesOtherwiseTemplate}.
%
% The optional argument \meta{extra} is some text to insert after the
% case head but before the line break. The default value is
% \seemacro{byCasesEveryOtherwise}.
% \begin{decl}
% \defmacro{icase} \oarg{rule-name} \marg{premises} \\
% | | \marg{conclusion} \oarg{where-clause}
% \\
% \hline
% \defmacro{icase*} \oarg{inferrule*-opts} \marg{premises} \\
% | | \marg{conclusion} \oarg{where-clause}
% \end{decl}
% These commands are defined only
% if the \textsf{mathpartir} package is detected or loaded explicitly
% with the \seeoption{mathpartir} option. In that case, they typeset
% a case using an inference rule. The non-starred variant uses
% \usemacro{inferrule} and the starred variant uses
% \usemacro{inferrule*}. Thus, the first optional argument to |icase|
% is a rule name and the first optional argument to |icase*| is a
% key-value list of options understood by |\inferrule*|.
%
% The second
% and third arguments are the premises and conclusion to put in the
% inference rule.
%
% Then, the final, optional argument, allows
% specifying a side condition, which will be printed after the
% inference rule like
% ``~\textbf{where}~|$|\meta{where-clause}|$|\textbf.'' The text can
% be changed by redefining \seeoption{byCasesWhereTemplate}.
% \end{quotation}
%
% \begin{decl}
% \defmacro{byCasesEveryCase} \\
% \hline
% \defmacro{byCasesEveryOtherwise}
% \end{decl}
% These are the default values for the optional argument \oarg{extra} of
% |\case| and |\otherwise|. The initial value of |\byCasesEveryCase| is
% \seemacro{resetpfcounter}, so that every case implicitly resets the
% proof counter. The initial value of |\byCasesEveryOtherwise| points to
% |\byCasesEveryCase|. These can be redefined to avoid automatic proof
% counter resets, or to change the behavior of |\case| and |\otherwise|
% in some other ways. Or, they can be ignored on a case-by-case basis
% by passing a blank for \meta{extra}.
%
% \begin{decl}
% \textbf{command} & \textbf{default} \\
% \hline
% \hline
% \defmacro{byCasesCaseTemplate} \marg{case-text}
% & |\textbf{Case |\marg{case-text}|.}|
% \\
% \hline
% \defmacro{byCasesOtherwiseTemplate}
% & |\textbf{Otherwise.}|
% \\
% \hline
% \defmacro{byCasesWhereTemplate}
% & |\textbf{where}|
% \end{decl}
% These are used by the |\case|, |\otherwise|, and |\icase| templates to
% create the text ``Case,'' ``Otherwise'', and ``where'' along with the
% styling. Redefine them to change how these are presented.
%
% \StopEventually{
% \PrintChanges
% \setcounter{IndexColumns}{2}
% \clearpage
% \PrintIndex
% }
%
% \section{Implementation}
%
% We begin by loading the \textsf{listproc} package:
% \begin{macrocode}
\RequirePackage{listproc}
% \end{macrocode}
% \subsection{Package Options}
% \begin{macros}{pfsteps@set,pfsteps@option}
% These macros make it easy to add package options. Each use of
% |\pfsteps@option|\marg{name} creates both the named option \meta{name}
% and its opposite, |no|\meta{name}, and sets things up so that we can
% detect whether an option has been explicitly set, explicitly unset, or
% left to default.
% \begin{macrocode}
\newcommand*\pfsteps@set[3][]{
\expandafter\let\csname #1pfsteps@#2\endcsname#3
}
\newcommand*\pfsteps@option[2][\iffalse]{
\pfsteps@set[if]{#2}#1
\pfsteps@set[if]{#2@set}\iffalse
\DeclareOption{#2}{
\pfsteps@set[if]{#2}\iftrue
\pfsteps@set[if]{#2@set}\iftrue
}
\DeclareOption{no#2}{
\pfsteps@set[if]{#2}\iffalse
\pfsteps@set[if]{#2@set}\iftrue
}
}
% \end{macrocode}
% \end{macros}
% \begin{macros}{ifpfsteps@atsign,ifpfsteps@atsign@set,ifpfsteps@hyperref,ifpfsteps@hyperref@set,ifpfsteps@loadunicode,ifpfsteps@loadunicode@set,ifpfsteps@mathpartir,ifpfsteps@mathpartir@set,ifpfsteps@unicode,ifpfsteps@unicode@set}
% This sets up all the options. The first four of them default to
% \emph{true}. Then, we process the package options.
% \begin{macrocode}
\pfsteps@option[\iftrue]{atsign}
\pfsteps@option[\iftrue]{hyperref}
\pfsteps@option[\iftrue]{loadunicode}
\pfsteps@option[\iftrue]{mathpartir}
\pfsteps@option{unicode}
\ProcessOptions
% \end{macrocode}
% \end{macros}
% If both the \seeoption{unicode} and \seeoption{loadunicode} options
% are set, we load the relevant packages.
% \begin{macrocode}
\ifpfsteps@unicode
\ifpfsteps@loadunicode
\RequirePackage{ucs}
\RequirePackage[utf8x]{inputenc}
\fi
\fi
% \end{macrocode}
% If \seeoption{mathpartir} has been explicitly set, load it.
% \begin{macrocode}
\ifpfsteps@mathpartir
\ifpfsteps@mathpartir@set
\RequirePackage{mathpartir}
\fi
\fi
% \end{macrocode}
% If \seeoption{hyperref} has been explicitly set, load it.
% \begin{macrocode}
\ifpfsteps@hyperref
\ifpfsteps@hyperref@set
\RequirePackage{hyperref}
\fi
\fi
% \end{macrocode}
% \subsection{Proof Step Numbering}
% This section is based on Didier R\'emy’s \textsf{locallabel} package.
% It differs in terms of the protocol for when proof steps are defined
% versus displayed.
% \begin{macros}{pfcounteranchor,pfcounterref}
% User redefinable commands for formatting proof step numbers:
% \begin{macrocode}
\newcommand{\pfcounteranchor}[1]{(#1)}
\newcommand{\pfcounterref}[1]{(#1)}
% \end{macrocode}
% \end{macros}
% \begin{macros}{c@pfsteps@pfc@global,c@pfsteps@pfc@local}
% Two counters for proof steps, one to keep track of how many times
% we've reset the count, and the other to keep the current step count.
% \begin{macrocode}
\newcounter{pfsteps@pfc@global}
\newcounter{pfsteps@pfc@local}
% \end{macrocode}
% \end{macros}
% \begin{macros}{resetpfcounter,thepfcounter,thepfsectioncounter,steppfcounter}
% Simple counter management:
% \begin{macrocode}
\newcommand{\resetpfcounter}[1][0]
{\stepcounter{pfsteps@pfc@global}\setcounter{pfsteps@pfc@local}{#1}}
\newcommand{\thepfcounter}
{\the\value{pfsteps@pfc@local}}
\newcommand{\thepfsectioncounter}
{\the\value{pfsteps@pfc@global}}
\newcommand{\steppfcounter}[1][\relax]{%
\addtocounter{pfsteps@pfc@local}{1}%
\ifx\relax#1\relax\else
\pflabel{#1}%
\fi
}
% \end{macrocode}
% \end{macros}
% \begin{macros}{usepfcounter}
% To advance and print the proof counter. We use
% \usemacro{pfsteps@hypertarget}, which delegates to
% \usemacro{hypertarget} if \textsf{hyperref} has been detected.
% \begin{macrocode}
\newcommand{\usepfcounter}[1][\relax]{%
\steppfcounter[#1]%
\pfsteps@hypertarget{pfc:\thepfsectioncounter:\thepfcounter}{%
\pfcounteranchor{\thepfcounter}%
}%
}
% \end{macrocode}
% \end{macros}
% \begin{macros}{pfsteps@pfc@cs,pfsteps@pfc@,pfsteps@strip}
% These are helper macros for turning a proof label name into the name
% of the command that we store its number in. |\pfsteps@pfc@cs|
% actually returns the control sequence, whereas |\pfsteps@pfc@| just
% returns the name of the control sequence. Both use |\pfsteps@strip|
% to remove spaces from the proof label.
% \begin{macrocode}
\newcommand{\pfsteps@pfc@cs}[1]
{\csname\pfsteps@pfc@{\pfsteps@strip#1 \@empty}\endcsname}
\newcommand{\pfsteps@pfc@}[1]
{pfsteps@pfc@\pfsteps@strip#1 \@empty @\thepfsectioncounter}
\def\pfsteps@strip#1 #2{%
#1%
\ifx#2\@empty\else\expandafter\pfsteps@strip\fi
#2}
% \end{macrocode}
% \end{macros}
% \begin{macros}{pflabel}
% This associates a name with the current state of the proof counter.
% It both defines a macro in current session for producing backward proof step
% references write away, and writes code to the auxiliary file so that
% forward proof step referenced work in the next run. To make this work
% smoothly, it actually defines two macros whose names are based on the
% current proof state. The main one is used to hold the proof step
% number. The extra macro, which ends with |@thisrun|, is defined for
% the current session but not in the auxiliary file. We can then use
% |@thisrun| to detect attempts to reuse the same label name in the same
% proof section in the same run, in order to issue a warning.
% \begin{macrocode}
\newcommand{\pflabel}[1]
{\expandafter\ifx\csname\pfsteps@pfc@{#1}@thisrun\endcsname\relax
\expandafter\xdef\csname\pfsteps@pfc@{#1}\endcsname
{\thepfcounter}%
\expandafter\gdef\csname\pfsteps@pfc@{#1}@thisrun\endcsname
{}%
\immediate\write\@auxout{
\noexpand\pfsteps@def@label
{#1}{\thepfsectioncounter}{\thepfcounter}
}%
\else
\PackageWarning{pfsteps}
{Proof step (#1) already defined in this section}%
\fi}
% \end{macrocode}
% \end{macros}
% \begin{macros}{pfsteps@def@label}
% This is the command written to the auxiliary file, so we have it
% defined here in order to run it when loading the auxiliary file.
% \begin{macrocode}
\newcommand*{\pfsteps@def@label}[3]{
\expandafter\gdef
\csname pfsteps@pfc@#1@#2\endcsname
{#3}
}
% \end{macrocode}
% \end{macros}
% \begin{macros}{pfref}
% For creating proof step references. The bulk of this is a large
% \textsf{listproc} list expression, which does several steps: parse the
% argument as a comma-separated list of label names; map over those
% names to build pairs of the raw number as a sorting key and the
% formatted (possibly hyperlinked) references, or suitable error
% messages if the label isn't defined; sort by the numeric key, which is
% the proof step number, and compress adjacent keys into ranges.
% \begin{macrocode}
\newcommand*{\pfref}[1]
{{\ListExprTo
{\Compress[\@apply@group\@firstoftwo]
{\Sort[\@apply@group\@firstoftwo]
{\Map
{%
{\@ifundefined{\pfsteps@pfc@{##1}}
{-1}
{\csname\pfsteps@pfc@{##1}\endcsname}}%
{\@ifundefined{\pfsteps@pfc@{##1}}
{\PackageWarning{pfsteps}
{Proof step (##1) not yet defined in this section}%
\textbf{?}}
{\pfsteps@hyperlink
{pfc:\thepfsectioncounter:\pfsteps@pfc@cs{##1}}
{\pfsteps@pfc@cs{##1}}}}}
{\List{#1}}}}}
\pfsteps@pfref@list
% \end{macrocode}
% We finish up by setting singleton proof steps to print as-is and
% ranges to print with en dashes. We set \usemacro{listitem} to print
% the first list item with no punctuation and to redefine itself to
% print commas for subsequent items.
% \begin{macrocode}
\let\listitem\pfsteps@pfref@listitem@first
\def\@single##1{\@secondoftwo##1}%
\def\@range##1##2{\@secondoftwo##1--\@secondoftwo##2}%
\pfcounterref{\pfsteps@pfref@list}%
}}
% \end{macrocode}
% \end{macros}
% \begin{macros}{pfsteps@pfref@listitem@first,pfsteps@pfref@listitem@rest}
% |\pfref| uses these to print a comma separated list.
% \begin{macrocode}
\newcommand\pfsteps@pfref@listitem@first[1]{%
#1\let\listitem\pfsteps@pfref@listitem@rest
}
\newcommand\pfsteps@pfref@listitem@rest[1]{%
, #1\let\listitem\pfsteps@pfref@listitem@rest
}
% \end{macrocode}
% \end{macros}
% \begin{macros}{pfsteps@hypertarget,pfsteps@hyperlink}
% This is the \textsf{hyperref} compatibility layer. We initially define
% our compatibility commands to ignore the first argument (which is an
% anchor name) and just print the second. Then, if the
% \seeoption{hyperref} option is enabled, either by default or by
% choice, we wait until the preamble ends and attempt to detect
% \textsf{hyperref}. If it's detected, we redefine the compatibility
% macros to use the real things.
% \begin{macrocode}
\newcommand\pfsteps@hypertarget[2]{#2}
\newcommand\pfsteps@hyperlink[2]{#2}
\ifpfsteps@hyperref
\AtBeginDocument{
\ifcsname hypertarget\endcsname
\let\pfsteps@hypertarget=\hypertarget
\let\pfsteps@hyperlink=\hyperlink
\fi
}
\fi
% \end{macrocode}
% \end{macros}
% \subsection{Proof Sequences}
% \begin{macros}{proofleftskip,proofrightwidth}
% Length parameters for configuring spacing of the |pfsteps|
% environment.
% \begin{macrocode}
\newlength{\proofleftskip}
\newlength{\proofrightwidth}
\setlength{\proofleftskip}{2pc}
\setlength{\proofrightwidth}{0.3\linewidth}
% \end{macrocode}
% \end{macros}
% \begin{environment}{pfsteps}
% \changes{v0.4}{2011/04/04}{Spacing bug fixes: Sets parskip to 0pt,
% so we don't get really wide spacing in proofs. Avoids weird behavior
% when proof steps are too long.}
% \begin{environment}{pfsteps*}
% The |pfsteps| and |pfsteps*| environments are both defined in terms of
% the underlying |pfsteps@with| environment, which takes an argument to
% determine whether proof steps are in math mode.
% \begin{macrocode}
\newenvironment{pfsteps}
{\begin{pfsteps@with}$}
{\end{pfsteps@with}}
\newenvironment{pfsteps*}
{\begin{pfsteps@with}{}}
{\end{pfsteps@with}}
% \end{macrocode}
% \end{environment}
% \end{environment}
% \begin{environment}{pfsteps@with}
% The implementation of the |pfsteps| environment. The whole thing is
% set in a \usemacro{trivlist}, using \usemacro{item} for line breaks.
% \begin{macrocode}
\newenvironment{pfsteps@with}[1]
{
\leavevmode\begingroup
\setlength{\parskip}{0pt}%
\trivlist
\raggedright
\setlength{\leftskip}{1.5\proofleftskip}
% \end{macrocode}
% Save some commands that we want to redefine in here.
% \begin{macrocode}
\let\pfstepsSavedItem\item
\let\pfstepsSavedLabel\label
\let\pfstepsSavedQedhere\qedhere
% \end{macrocode}
% \begin{macros}{AND,BY,item,label,qedhere}
% We then setup several commands that are internal to the environment.
% The interesting ones are |\BY| and |\item|. For |\BY|, we break out
% of math mode if we're in it, and then set the justification in a
% minipage of the configured with. However, right before the minipage,
% we use |\penalty-1| to encourage a page break if there isn't enough
% room left on the line for the justification box, and then we |\hfill|
% to right align it. The result is that justifications appear cleanly
% to the right of proof steps, on new lines only when necessary.
% \begin{macrocode}
\newcommand\AND[1][and]{\mathrel{\mbox{##1}}}
\newcommand\BY[2][by]
{\pfsteps@unmath{\penalty-1 \mbox{~}\hfill%
\begin{minipage}[t]{\proofrightwidth}%
\raggedright##1 ##2%
\end{minipage}}}
% \end{macrocode}
% For |\item|, we break out of math mode if necessary, then start a new
% underlying |\item|, generate a proof step number, and optionall go
% back into math mode.
% \begin{macrocode}
\def\pfstepsItem{%
\pfsteps@stopmath
\pfstepsSavedItem\mbox{}\kern-1.25\proofleftskip
\makebox[\proofleftskip]{\hfill\usepfcounter}\kern0.25\proofleftskip
#1\relax}
% \end{macrocode}
% For |\qedhere|, we need to temporarily break out of math mode, or the
% QED box ends up in a weird place.
% \begin{macrocode}
\def\pfstepsQedhere{\pfsteps@unmath{\pfstepsSavedQedhere}}
% \end{macrocode}
% We redefine |\item|, |\label|, and |\qedhere| to use the proof steps
% versions of the same.
% \begin{macrocode}
\let\item\pfstepsItem
\let\label\pflabel
\let\qedhere\pfstepsQedhere
% \end{macrocode}
% \end{macros}
% \begin{macrocode}
\ifpfsteps@atsign
\pfsteps@setup@atsign
\fi
\relax
}
{
\pfsteps@stopmath
\endtrivlist\endgroup
\noindent\ignorespaces
}
% \end{macrocode}
% \end{environment}
% \begin{macros}{pfsteps@stopmath,pfsteps@unmath}
% Two commands for getting us out of math mode, but only if we're in it.
% |\pfsteps@unmath| takes an argument to set outside of math mode, and
% then reinstates math mode only if we were in math mode to begin with.
% This is useful compared to creating an |\mbox| in math mode, because
% it \emph{ends} the current math environment, which will then let us do
% something like start a new list item before entering math mode again.
% \begin{macrocode}
\newcommand\pfsteps@stopmath{\ifmmode$\fi}
\newcommand\pfsteps@unmath[1]{\ifmmode$\relax#1\relax$\else\relax#1\relax\fi}
% \end{macrocode}
% \end{macros}
% \begin{macros}{pfsetps@setup@atsign}
% A macro to make |@| active and define it to alias |\pflabel|. A bit
% tricky, since we also want |@| in the name of the command.
% \begin{macrocode}
{
\def\atsign{@}
\catcode`\@=\active\relax
\expandafter\gdef\csname pfsteps\atsign setup\atsign atsign\endcsname{
\catcode`\@=\active\relax
\gdef@##1 {\pflabel{##1}}
}
}
% \end{macrocode}
% \end{macros}
% \begin{macros}{pfstepsmathmode,pfstepstextmode}
% Commands to determine whether the Unicode short hand is in math or
% text mode.
% \begin{macrocode}
\newcommand\pfstepsmathmode{\def\pfsteps@unicode@arg{$}}
\newcommand\pfstepstextmode{\def\pfsteps@unicode@arg{\relax}}
% \end{macrocode}
% \end{macros}
% \begin{macros}{pfstepsSetupUnicode,pfsteps@unicode@startpfsteps,pfsteps@unicode@startpfsteps@kont,pfsteps@unicode@item}
% For setting up the Unicode |pfsteps| shortcut. This associates the
% code points of the start and item sequences with commands that
% implement them, and then defines those commands. We default to math
% mode.
% \begin{macrocode}
\newcommand\pfstepsSetupUnicode[3]{
\DeclareUnicodeCharacter{#1}{\pfsteps@unicode@startpfsteps}
\DeclareUnicodeCharacter{#3}{\pfsteps@unicode@item}
\def\pfsteps@unicode@startpfsteps
{\begingroup
\ifpfsteps@atsign\catcode`\@=\active\relax\fi
\pfsteps@unicode@startpfsteps@kont}
\def\pfsteps@unicode@startpfsteps@kont##1#2
{\begin{pfsteps@with}\pfsteps@unicode@arg\item##1\end{pfsteps@with}%
\endgroup}
\def\pfsteps@unicode@item{\item}
\pfstepsmathmode
}
% \end{macrocode}
% \end{macros}
% If the \seeoption{unicode} option is set, then we setup unicode with
% left and right guillemets as the delimiters and bullet as the item
% separator. The second argument to |\pfstepsSetupUnicode| below, which
% appears empty in the documentation, is the right guillemet \ttrguil.
% The two numbers, 171 and 8226, are the code
% points for left guillemet and bullet, respectively.
% \changes{v0.3}{2011/03/31}{Input encoding bug fix for right guillemet}
% \begin{macrocode}
\ifpfsteps@unicode
\pfstepsSetupUnicode{171}{»}{8226} % « » •
\fi
% \end{macrocode}
% \subsection{The \texttt{byCases} Environment}
%
% \begin{macros}{byCasesEveryCase,byCasesEveryOtherwise,byCasesOtherwiseTemplate,byCasesCaseTemplate,byCasesWhereTemplate}
% User configuration macros. The first two cause the proof
% step to be automatically reset for every case item, and the last three
% specify how case items are to appear.
% \begin{macrocode}
\newcommand\byCasesEveryCase{\resetpfcounter}
\newcommand\byCasesEveryOtherwise{\byCasesEveryCase}
\providecommand{\byCasesOtherwiseTemplate}{\textbf{Otherwise.}}
\providecommand{\byCasesCaseTemplate}[1]{\textbf{Case {#1}.}}
\providecommand{\byCasesWhereTemplate}{\textbf{where}}
% \end{macrocode}
% \end{macros}
% \begin{environment}{byCases}
% This environment is based on the |description| environment built-in to
% \LaTeX. However, we also bring |\case| and |\otherwise| into scope by
% aliasing them to the actual definitions (below).
% \begin{macrocode}
\newenvironment{byCases}
{%
\begingroup
\let\case\byCases@case
\let\otherwise\byCases@otherwise
% \end{macrocode}
% Package \textsf{mathpartir} integration: if the option is set and the
% command is in scope, then we bring |\icase| into scope.
% \begin{macrocode}
\ifpfsteps@mathpartir
\ifcsname inferrule\endcsname\let\icase\byCases@icase\fi
\fi
\list{}{\labelwidth\z@ \itemindent-\leftmargin
\let\makelabel\byCases@label}%
}
{%
\endlist
\endgroup
}
% \end{macrocode}
% \end{environment}
% \begin{macros}{item}
% This is the implementation of |\item| labels for |byCases| lists.
% \begin{macrocode}
\newcommand*\byCases@label[1]{%
\hspace\labelsep
\normalfont~\strut
\expandafter\ifx#1\relax\relax
\byCasesOtherwiseTemplate
\else
\byCasesCaseTemplate{\normalfont${#1}$}%
\fi
}
% \end{macrocode}
% \end{macros}
% \begin{macros}{case,otherwise,AND,byCases@case,byCases@otherwise,pfsteps@reallynopagebreak}
% These are the actual definitions of |\case| and |\otherwise| that
% |\byCases| brings into scope with accessible names. Mostly, they
% delegate to |\item| and then produce a line break while suppressing
% any page break. In |\case|, it defines |\AND| to produce a properly
% spaced text `` and '' in math mode, just for the scope of
% the item label.
% \begin{macrocode}
\newcommand*\byCases@case[2][\byCasesEveryCase]
{\item[{\let\AND\byCases@and #2}]\strut#1\pfsteps@reallynopagebreak}
\newcommand*\byCases@otherwise[1][\byCasesEveryOtherwise]
{\item[]\strut#1\pfsteps@reallynopagebreak}
\newcommand\pfsteps@reallynopagebreak{\par\nopagebreak\@nobreaktrue}
\newcommand\byCases@and[1][and]{\mathrel{\mbox{\textbf{#1}}}}
% \end{macrocode}
% \end{macros}
% \begin{macros}{icase,byCases@icase,byCases@icase@start,byCases@icase@nostar}
% The first thing |\icase| does is detect whether it is being called as
% |\icase| or as |\icase*| and dispatches accordingly. These then
% select either \usemacro{inferrule} or \usemacro{inferrule*}.
% \begin{macrocode}
\newcommand*\byCases@icase{
\@ifnextchar* \byCases@icase@star \byCases@icase@nostar
}
\def\byCases@icase@nostar{\byCases@icase@i{\inferrule}}
\def\byCases@icase@star*{\byCases@icase@i{\inferrule*}}
% \end{macrocode}
% \end{macros}
% \begin{macros}{byCases@icase@i,byCases@icase@opts,byCases@icase@noopts}
% The next thing to check for is the first optional argument; we
% dispatch accordingly and pass the version of |inferrule| to use along
% with the optional argument, if necessary, to |byCases@icase@ii|.
% \begin{macrocode}
\newcommand*\byCases@icase@i[1]{
\@ifnextchar [{\byCases@icase@opts{#1}}{\byCases@icase@noopts{#1}}
}
\def\byCases@icase@opts#1[#2]{\byCases@icase@ii{#1[#2]}}
\def\byCases@icase@noopts#1{\byCases@icase@ii{#1}}
% \end{macrocode}
% \end{macros}
% \begin{macros}{byCases@icase@ii,byCases@icase@where,byCases@icase@nowhere}
% This macro receives three arguments: (|#1|) the variant of |inferrule|
% along with any optional argument, (|#2|) the premises, and (|#3|) the
% conclusion. It then checks for the final, optional argument which
% specifies a where clause, and dispatches accordingly.
% \begin{macrocode}
\newcommand*\byCases@icase@ii[3]{
\@ifnextchar [
{\byCases@icase@where{#1}{#2}{#3}}
{\byCases@icase@nowhere{#1}{#2}{#3}}
}
\def\byCases@icase@where#1#2#3[#4]{
\case{#1{#2}{#3}\AND[\byCasesWhereTemplate]#4}%
}
\def\byCases@icase@nowhere#1#2#3{\case{#1{#2}{#3}}}
% \end{macrocode}
% \end{macros}
%
% \Finale
%
\endinput