summaryrefslogtreecommitdiff
path: root/macros/latex/contrib/fitch/fitch.sty
diff options
context:
space:
mode:
Diffstat (limited to 'macros/latex/contrib/fitch/fitch.sty')
-rw-r--r--macros/latex/contrib/fitch/fitch.sty346
1 files changed, 215 insertions, 131 deletions
diff --git a/macros/latex/contrib/fitch/fitch.sty b/macros/latex/contrib/fitch/fitch.sty
index 59e06c5a61..a1dc1fc9f4 100644
--- a/macros/latex/contrib/fitch/fitch.sty
+++ b/macros/latex/contrib/fitch/fitch.sty
@@ -18,9 +18,9 @@
% Original Author: Peter Selinger, Dalhousie University
% Created: Jan 14, 2002
-% Modified: Sep 4, 2023
-% Version: 0.6
-% Copyright: (C) 2002-2005 Peter Selinger
+% Modified: December 17, 2023
+% Version: 1.0
+% Copyright: (C) 2002-2005 Peter Selinger, Richard Zach
% Filename: fitch.sty
% Documentation: fitchdoc.tex
% https://github.com/OpenLogicProject/fitch/
@@ -50,159 +50,222 @@
% \]
\NeedsTeXFormat{LaTeX2e}
-\ProvidesPackage{fitch}[2023-09-04 v0.6 Macros for Fitch-style natural deduction]
+\ProvidesPackage{fitch}[2023-12-17 v1.0 Macros for Fitch-style natural deduction]
-{\chardef\x=\catcode`\*
-\catcode`\*=11
-\global\let\nd*astcode\x}
-\catcode`\*=11
+% Define keyval options
+
+\RequirePackage{kvoptions}
+
+\SetupKeyvalOptions{
+family = fitch,
+prefix = nd@ % prefix with nd@ for compatibility with old code
+}
+
+\DeclareStringOption[ndrules]{rules}
+\DeclareStringOption[array]{arrayenv}
+\DeclareStringOption[ndjustformat]{justformat}
+\DeclareStringOption[ndrefformat]{refformat}
+
+\DeclareStringOption[4.5ex]{height}[4.5ex]
+\DeclareStringOption[3.5ex]{topheight}[3.5ex]
+\DeclareStringOption[1.5ex]{depth}[1.5ex]
+\DeclareStringOption[1em]{labelsep}[1em]
+\DeclareStringOption[1.6em]{indent}[1.6em]
+\DeclareStringOption[1.5ex]{hsep}[1.5ex]
+\DeclareStringOption[2.5em]{justsep}[2.5em]
+\DeclareStringOption[.2mm]{linethickness}[.2mm]
+\DeclareStringOption[1em]{cindent}[1em]
+\DeclareBoolOption[true]{outerline}
+
+% user command to redefine dimensions
+\def\nddim#1#2#3#4#5#6#7#8{
+ \setkeys{fitch}{
+ height=#1,
+ topheight=#2,
+ depth=#3,
+ labelsep=#4,
+ indent=#5,
+ hsep=#6,
+ justsep=#7,
+ linethickness=#8
+ }
+}
+
+\DeclareLocalOptions{
+ rules,
+ arrayenv,
+ justformat,
+ refformat,
+ height,
+ topheight,
+ depth,
+ labelsep,
+ indent,
+ hsep,
+ justsep,
+ linethickness,
+ cindent,
+ outerline
+}
+
+\ProcessLocalKeyvalOptions{fitch}
+
+% Actual fitch.sty code
+
+\newlength{\nd@dim}
% References
-\newcount\nd*ctr
-\def\nd*render{\expandafter\ifx\expandafter\nd*x\nd*base\nd*x\the\nd*ctr\else\nd*base\ifnum\nd*ctr<0\the\nd*ctr\else\ifnum\nd*ctr>0+\the\nd*ctr\fi\fi\fi}
-\expandafter\def\csname nd*-\endcsname{}
-
-\def\nd*num#1{\nd*numo{\nd*render}{#1}\global\advance\nd*ctr1}
-\def\nd*numopt#1#2{\nd*numo{$#1$}{#2}}
-\def\nd*numo#1#2{\edef\x{#1}\mbox{$\x$}\expandafter\global\expandafter\let\csname nd*-#2\endcsname\x}
-\def\nd*ref#1{\expandafter\let\expandafter\x\csname nd*-#1\endcsname\ifx\x\relax%
- \PackageWarning{fitch}{Undefined line reference: #1}\mbox{\textbf{??}}\else\mbox{$\x$}\fi}
-\def\nd*noop{}
-\def\nd*set#1#2{\ifx\relax#1\nd*noop\else\global\def\nd*base{#1}\fi\ifx\relax#2\relax\else\global\nd*ctr=#2\fi}
-\def\nd*reset{\nd*set{}{1}}
-\def\nd*refa#1{\nd*ref{#1}}
-\def\nd*aux#1#2{\ifx#2-\nd*refa{#1}--\def\nd*c{\nd*aux{}}%
- \else\ifx#2,\nd*refa{#1}, \def\nd*c{\nd*aux{}}%
- \else\ifx#2;\nd*refa{#1}; \def\nd*c{\nd*aux{}}%
- \else\ifx#2.\nd*refa{#1}. \def\nd*c{\nd*aux{}}%
- \else\ifx#2)\nd*refa{#1})\def\nd*c{\nd*aux{}}%
- \else\ifx#2(\nd*refa{#1}(\def\nd*c{\nd*aux{}}%
- \else\ifx#2\nd*end\nd*refa{#1}\def\nd*c{}%
- \else\def\nd*c{\nd*aux{#1#2}}%
- \fi\fi\fi\fi\fi\fi\fi\nd*c}
-\def\ndref#1{\nd*aux{}#1\nd*end}
+\newcount\nd@ctr
+\def\nd@render{\expandafter\ifx\expandafter\nd@x\nd@base\nd@x\the\nd@ctr\else\nd@base\ifnum\nd@ctr<0\the\nd@ctr\else\ifnum\nd@ctr>0+\the\nd@ctr\fi\fi\fi}
+\expandafter\def\csname nd@-\endcsname{}
+
+\def\nd@num#1{\nd@numo{\nd@render}{#1}\global\advance\nd@ctr1}
+\def\nd@numopt#1#2{\nd@numo{$#1$}{#2}}
+\def\nd@numo#1#2{\edef\x{#1}\mbox{$\x$}\expandafter\global\expandafter\let\csname nd@-#2\endcsname\x}
+\def\nd@ref#1{\expandafter\let\expandafter\x\csname nd@-#1\endcsname\ifx\x\relax%
+ \PackageWarning{fitch}{Undefined line reference: #1}\mbox{\textbf{??}}\else\csname\nd@refformat\endcsname{\mbox{$\x$}}\fi}
+\def\nd@noop{}
+\def\nd@set#1#2{\ifx\relax#1\nd@noop\else\global\def\nd@base{#1}\fi\ifx\relax#2\relax\else\global\nd@ctr=#2\fi}
+\def\nd@reset{\nd@set{}{1}}
+\def\nd@refa#1{\nd@ref{#1}}
+\def\nd@aux#1#2{\ifx#2-\nd@refa{#1}--\def\nd@c{\nd@aux{}}%
+ \else\ifx#2,\nd@refa{#1}, \def\nd@c{\nd@aux{}}%
+ \else\ifx#2;\nd@refa{#1}; \def\nd@c{\nd@aux{}}%
+ \else\ifx#2.\nd@refa{#1}. \def\nd@c{\nd@aux{}}%
+ \else\ifx#2)\nd@refa{#1})\def\nd@c{\nd@aux{}}%
+ \else\ifx#2(\nd@refa{#1}(\def\nd@c{\nd@aux{}}%
+ \else\ifx#2\nd@end\nd@refa{#1}\def\nd@c{}%
+ \else\def\nd@c{\nd@aux{#1#2}}%
+ \fi\fi\fi\fi\fi\fi\fi\nd@c}
+\def\ndref#1{\nd@aux{}#1\nd@end}
% Layer A
-% define various dimensions (explained in fitchdoc.tex):
-\newlength{\nd*dim}
-\newdimen\nd*depthdim
-\newdimen\nd*hsep
-\newdimen\ndindent
-\ndindent=1em
-% user command to redefine dimensions
-\def\nddim#1#2#3#4#5#6#7#8{\nd*depthdim=#3\relax\nd*hsep=#6\relax%
-\def\nd*height{#1}\def\nd*thickness{#8}\def\nd*initheight{#2}%
-\def\nd*indent{#5}\def\nd*labelsep{#4}\def\nd*justsep{#7}}
% set initial dimensions
-\nddim{4.5ex}{3.5ex}{1.5ex}{1em}{1.6em}{.5em}{2.5em}{.2mm}
+%\nddim{4.5ex}{3.5ex}{1.5ex}{1em}{1.6em}{.5em}{2.5em}{.2mm}
-\def\nd*v{\rule[-\nd*depthdim]{\nd*thickness}{\nd*height}}
-\def\nd*t{\rule[-\nd*depthdim]{0mm}{\nd*height}\rule[-\nd*depthdim]{\nd*thickness}{\nd*initheight}}
-\def\nd*i{\hspace{\nd*indent}}
-\def\nd*s{\hspace{\nd*hsep}}
-\def\nd*g#1{\nd*f{\makebox[\nd*indent][c]{$#1$}}}
-\def\nd*f#1{\raisebox{0pt}[0pt][0pt]{$#1$}}
-\def\nd*u#1{\makebox[0pt][l]{\settowidth{\nd*dim}{\nd*f{#1}}%
- \addtolength{\nd*dim}{2\nd*hsep}\hspace{-\nd*hsep}\rule[-\nd*depthdim]{\nd*dim}{\nd*thickness}}\nd*f{#1}}
+\def\nd@v{\rule[-\nd@depth]{\nd@linethickness}{\nd@height}}
+\def\nd@h{\rule[-\nd@depth]{0mm}{\nd@height}} % strut
+\def\nd@t{\rule[-\nd@depth]{\nd@linethickness}{\nd@topheight}}
+\def\nd@i{\hspace{\nd@indent}}
+\def\nd@s{\hspace{\nd@hsep}}
+\def\nd@g#1{\nd@f{\makebox[\nd@indent][c]{$#1$}}}
+\def\nd@f#1{\raisebox{0pt}[0pt][0pt]{$#1$}}
+\def\nd@u#1{\makebox[0pt][l]{\settowidth{\nd@dim}{\nd@f{#1}}%
+ \addtolength{\nd@dim}{\nd@hsep}\addtolength{\nd@dim}{\nd@hsep}%
+ \hspace{-\nd@hsep}\rule[-\nd@depth]{\nd@dim}{\nd@linethickness}}\nd@f{#1}}
% Lists
-\def\nd*push#1#2{\expandafter\gdef\expandafter#1\expandafter%
- {\expandafter\nd*cons\expandafter{#1}{#2}}}
-\def\nd*pop#1{{\def\nd*nil{\gdef#1{\nd*nil}}\def\nd*cons##1##2%
+\def\nd@push#1#2{\expandafter\gdef\expandafter#1\expandafter%
+ {\expandafter\nd@cons\expandafter{#1}{#2}}}
+\def\nd@pop#1{{\def\nd@nil{\gdef#1{\nd@nil}}\def\nd@cons##1##2%
{\gdef#1{##1}}#1}}
-\def\nd*iter#1#2{{\def\nd*nil{}\def\nd*cons##1##2{##1#2{##2}}#1}}
-\def\nd*modify#1#2#3{{\def\nd*nil{\gdef#1{\nd*nil}}\def\nd*cons##1##2%
- {\advance#2-1 ##1\advance#2 1 \ifnum#2=1\nd*push#1{#3}\else%
- \nd*push#1{##2}\fi}#1}}
+\def\nd@iter#1#2{{\def\nd@nil{}\def\nd@cons##1##2{##1#2{##2}}#1}}
+\def\nd@modify#1#2#3{{\def\nd@nil{\gdef#1{\nd@nil}}\def\nd@cons##1##2%
+ {\advance#2-1 ##1\advance#2 1 \ifnum#2=1\nd@push#1{#3}\else%
+ \nd@push#1{##2}\fi}#1}}
-\def\nd*cont#1{{\def\nd*t{\nd*v}\def\nd*v{\nd*v}\def\nd*g##1{\nd*i}%
- \def\nd*i{\nd*i}\def\nd*nil{\gdef#1{\nd*nil}}\def\nd*cons##1##2%
- {##1\expandafter\nd*push\expandafter#1\expandafter{##2}}#1}}
+\def\nd@cont#1{{\def\nd@t{\nd@v}\def\nd@v{\nd@v}\def\nd@g##1{\nd@i}%
+ \def\nd@i{\nd@i}\def\nd@nil{\gdef#1{\nd@nil}}\def\nd@cons##1##2%
+ {##1\expandafter\nd@push\expandafter#1\expandafter{##2}}#1}}
% Layer B
-\newcount\nd*n
-\def\nd*beginb{\begingroup\nd*reset\gdef\nd*stack{\nd*nil}\nd*push\nd*stack{\nd*t}%
- \begin{array}{l@{\hspace{\nd*labelsep}}l@{\hspace{\nd*justsep}}l}}
-\def\nd*resumeb{\begingroup\begin{array}{l@{\hspace{\nd*labelsep}}l@{\hspace{\nd*justsep}}l}}
-\def\nd*endb{\end{array}\endgroup}
-\def\nd*hypob#1#2{\nd*f{\nd*num{#1}}&\nd*iter\nd*stack\relax\nd*cont\nd*stack\nd*s\nd*u{#2}&}
-\def\nd*haveb#1#2{\nd*f{\nd*num{#1}}&\nd*iter\nd*stack\relax\nd*cont\nd*stack\nd*s\nd*f{#2}&}
-\def\nd*havecontb#1#2{&\nd*iter\nd*stack\relax\nd*cont\nd*stack\nd*s\nd*f{\hspace{\ndindent}#2}&}
-\def\nd*hypocontb#1#2{&\nd*iter\nd*stack\relax\nd*cont\nd*stack\nd*s\nd*u{\hspace{\ndindent}#2}&}
+\newcount\nd@n
+\def\nd@beginb{%
+ \begingroup
+ \nd@reset
+ \gdef\nd@stack{\nd@nil}%
+ \nd@push\nd@stack{\nd@h}%
+ \ifnd@outerline
+ \nd@push\nd@stack{\nd@t}\fi
+ \begin{\nd@arrayenv}{l@{\hspace{\nd@labelsep}}l@{\hspace{\nd@justsep}}l}}
+\def\nd@resumeb{%
+ \begingroup
+ \begin{\nd@arrayenv}{l@{\hspace{\nd@labelsep}}l@{\hspace{\nd@justsep}}l}}
+\def\nd@endb{\end{\nd@arrayenv}\endgroup}
+\def\nd@hypob#1#2{\nd@f{\nd@num{#1}}&\nd@iter\nd@stack\relax\nd@cont\nd@stack\nd@s\nd@u{#2}&}
+\def\nd@haveb#1#2{\nd@f{\nd@num{#1}}&\nd@iter\nd@stack\relax\nd@cont\nd@stack\nd@s\nd@f{#2}&}
+\def\nd@havecontb#1#2{&\nd@iter\nd@stack\relax\nd@cont\nd@stack\nd@s\nd@f{\hspace{\nd@cindent}#2}&}
+\def\nd@hypocontb#1#2{&\nd@iter\nd@stack\relax\nd@cont\nd@stack\nd@s\nd@u{\hspace{\nd@cindent}#2}&}
-\def\nd*openb{\nd*push\nd*stack{\nd*i}\nd*push\nd*stack{\nd*t}}
-\def\nd*closeb{\nd*pop\nd*stack\nd*pop\nd*stack}
-\def\nd*guardb#1#2{\nd*n=#1\multiply\nd*n by 2 \nd*modify\nd*stack\nd*n{\nd*g{#2}}}
+\def\nd@openb{\nd@push\nd@stack{\nd@i}\nd@push\nd@stack{\nd@t}}
+\def\nd@closeb{\nd@pop\nd@stack\nd@pop\nd@stack}
+\def\nd@guardb#1#2{\nd@n=#1\multiply\nd@n by 2 \nd@modify\nd@stack\nd@n{\nd@g{#2}}}
% Layer C
-\def\nd*clr{\gdef\nd*cmd{}\gdef\nd*typ{\relax}}
-\def\nd*sto#1#2#3{\gdef\nd*typ{#1}\gdef\nd*byt{}%
- \gdef\nd*cmd{\nd*typ{#2}{#3}\nd*byt\\}}
-\def\nd*chtyp{\expandafter\ifx\nd*typ\nd*hypocontb\def\nd*typ{\nd*havecontb}\else\def\nd*typ{\nd*haveb}\fi}
-\def\nd*hypoc#1#2{\nd*chtyp\nd*cmd\nd*sto{\nd*hypob}{#1}{#2}}
-\def\nd*havec#1#2{\nd*cmd\nd*sto{\nd*haveb}{#1}{#2}}
-\def\nd*hypocontc#1{\nd*chtyp\nd*cmd\nd*sto{\nd*hypocontb}{}{#1}}
-\def\nd*havecontc#1{\nd*cmd\nd*sto{\nd*havecontb}{}{#1}}
-\def\nd*by#1#2{\ifx\nd*x#2\nd*x\gdef\nd*byt{\mbox{#1}}\else\gdef\nd*byt{\mbox{#1, \ndref{#2}}}\fi}
+\def\nd@clr{\gdef\nd@cmd{}\gdef\nd@typ{\relax}}
+\def\nd@sto#1#2#3{\gdef\nd@typ{#1}\gdef\nd@byt{}%
+ \gdef\nd@cmd{\nd@typ{#2}{#3}\nd@byt\\}}
+\def\nd@chtyp{\expandafter\ifx\nd@typ\nd@hypocontb\def\nd@typ{\nd@havecontb}\else\def\nd@typ{\nd@haveb}\fi}
+\def\nd@hypoc#1#2{\nd@chtyp\nd@cmd\nd@sto{\nd@hypob}{#1}{#2}}
+\def\nd@havec#1#2{\nd@cmd\nd@sto{\nd@haveb}{#1}{#2}}
+\def\nd@hypocontc#1{\nd@chtyp\nd@cmd\nd@sto{\nd@hypocontb}{}{#1}}
+\def\nd@havecontc#1{\nd@cmd\nd@sto{\nd@havecontb}{}{#1}}
+\def\nd@by#1#2{\ifx\nd@x#2\nd@x\gdef\nd@byt{\mbox{#1}}\else\ifx\nd@x#1\nd@x\gdef\nd@byt{\mbox{\ndref{#2}}}\else\gdef\nd@byt{\mbox{\csname\nd@justformat\endcsname{#1}{\ndref{#2}}}}\fi\fi\ignorespaces}
% multi-line macros
-\def\nd*mhypoc#1#2{\nd*mhypocA{#1}#2\\\nd*stop\\}
-\def\nd*mhypocA#1#2\\{\nd*hypoc{#1}{#2}\nd*mhypocB}
-\def\nd*mhypocB#1\\{\ifx\nd*stop#1\else\nd*hypocontc{#1}\expandafter\nd*mhypocB\fi}
-\def\nd*mhavec#1#2{\nd*mhavecA{#1}#2\\\nd*stop\\}
-\def\nd*mhavecA#1#2\\{\nd*havec{#1}{#2}\nd*mhavecB}
-\def\nd*mhavecB#1\\{\ifx\nd*stop#1\else\nd*havecontc{#1}\expandafter\nd*mhavecB\fi}
-\def\nd*mhypocontc#1{\nd*mhypocB#1\\\nd*stop\\}
-\def\nd*mhavecontc#1{\nd*mhavecB#1\\\nd*stop\\}
-
-\def\nd*beginc{\nd*beginb\nd*clr}
-\def\nd*resumec{\nd*resumeb\nd*clr}
-\def\nd*endc{\nd*cmd\nd*endb}
-\def\nd*openc{\nd*cmd\nd*clr\nd*openb}
-\def\nd*closec{\nd*cmd\nd*clr\nd*closeb}
-\let\nd*guardc\nd*guardb
+\def\nd@mhypoc#1#2{\nd@mhypocA{#1}#2\\\nd@stop\\}
+\def\nd@mhypocA#1#2\\{\nd@hypoc{#1}{#2}\nd@mhypocB}
+\def\nd@mhypocB#1\\{\ifx\nd@stop#1\else\nd@hypocontc{#1}\expandafter\nd@mhypocB\fi}
+\def\nd@mhavec#1#2{\nd@mhavecA{#1}#2\\\nd@stop\\}
+\def\nd@mhavecA#1#2\\{\nd@havec{#1}{#2}\nd@mhavecB}
+\def\nd@mhavecB#1\\{\ifx\nd@stop#1\else\nd@havecontc{#1}\expandafter\nd@mhavecB\fi}
+\def\nd@mhypocontc#1{\nd@mhypocB#1\\\nd@stop\\}
+\def\nd@mhavecontc#1{\nd@mhavecB#1\\\nd@stop\\}
+
+\def\nd@beginc{\nd@beginb\nd@clr}
+\def\nd@resumec{\nd@resumeb\nd@clr}
+\def\nd@endc{\nd@cmd\nd@endb}
+\def\nd@openc{\nd@cmd\nd@clr\nd@openb}
+\def\nd@closec{\nd@cmd\nd@clr\nd@closeb}
+\let\nd@guardc\nd@guardb
% Layer D
% macros with optional arguments spelled-out
-\def\nd*hypod[#1][#2]#3[#4]#5{\ifx\relax#4\relax\else\nd*guardb{1}{#4}\fi\nd*mhypoc{#3}{#5}\nd*set{#1}{#2}}
-\def\nd*haved[#1][#2]#3[#4]#5{\ifx\relax#4\relax\else\nd*guardb{1}{#4}\fi\nd*mhavec{#3}{#5}\nd*set{#1}{#2}}
-\def\nd*havecont#1{\nd*mhavecontc{#1}}
-\def\nd*hypocont#1{\nd*mhypocontc{#1}}
-\def\nd*base{undefined}
-\def\nd*opend[#1]#2{\nd*cmd\nd*clr\nd*openb\nd*guard{#1}#2}
-\def\nd*close{\nd*cmd\nd*clr\nd*closeb}
-\def\nd*guardd[#1]#2{\nd*guardb{#1}{#2}}
+\def\nd@hypod[#1][#2]#3[#4]#5{\ifx\relax#4\relax\else\nd@guardb{1}{#4}\fi\nd@mhypoc{#3}{#5}\nd@set{#1}{#2}\ignorespaces}
+\def\nd@haved[#1][#2]#3[#4]#5{\ifx\relax#4\relax\else\nd@guardb{1}{#4}\fi\nd@mhavec{#3}{#5}\nd@set{#1}{#2}\ignorespaces}
+\def\nd@havecont#1{\nd@mhavecontc{#1}}
+\def\nd@hypocont#1{\nd@mhypocontc{#1}}
+\def\nd@base{undefined}
+\def\nd@opend[#1]#2{\nd@cmd\nd@clr\nd@openb\nd@guard{#1}#2}
+\def\nd@close{\nd@cmd\nd@clr\nd@closeb}
+\def\nd@guardd[#1]#2{\nd@guardb{#1}{#2}}
% Handling of optional arguments.
-\def\nd*optarg#1#2#3{\ifx[#3\def\nd*c{#2#3}\else\def\nd*c{#2[#1]{#3}}\fi\nd*c}
-\def\nd*optargg#1#2#3{\ifx[#3\def\nd*c{#1#3}\else\def\nd*c{#2{#3}}\fi\nd*c}
-
-\def\nd*five#1{\nd*optargg{\nd*four{#1}}{\nd*two{#1}}}
-\def\nd*four#1[#2]{\nd*optarg{0}{\nd*three{#1}[#2]}}
-\def\nd*three#1[#2][#3]#4{\nd*optarg{}{#1[#2][#3]{#4}}}
-\def\nd*two#1{\nd*three{#1}[\relax][]}
-
-\def\nd*have{\nd*five{\nd*haved}}
-\def\nd*hypo{\nd*five{\nd*hypod}}
-\def\nd*open{\nd*optarg{}{\nd*opend}}
-\def\nd*guard{\nd*optarg{1}{\nd*guardd}}
-
-\def\nd*init{%
- \let\open\nd*open%
- \let\close\nd*close%
- \let\hypo\nd*hypo%
- \let\have\nd*have%
- \let\hypocont\nd*hypocont%
- \let\havecont\nd*havecont%
- \let\by\nd*by%
- \let\guard\nd*guard%
+\def\nd@optarg#1#2#3{\ifx[#3\def\nd@c{#2#3}\else\def\nd@c{#2[#1]{#3}}\fi\nd@c}
+\def\nd@optargg#1#2#3{\ifx[#3\def\nd@c{#1#3}\else\def\nd@c{#2{#3}}\fi\nd@c}
+
+\def\nd@five#1{\nd@optargg{\nd@four{#1}}{\nd@two{#1}}}
+\def\nd@four#1[#2]{\nd@optarg{0}{\nd@three{#1}[#2]}}
+\def\nd@three#1[#2][#3]#4{\nd@optarg{}{#1[#2][#3]{#4}}}
+\def\nd@two#1{\nd@three{#1}[\relax][]}
+
+\def\nd@have{\nd@five{\nd@haved}}
+\def\nd@hypo{\nd@five{\nd@hypod}}
+\def\nd@open{\nd@optarg{}{\nd@opend}}
+\def\nd@guard{\nd@optarg{1}{\nd@guardd}}
+
+\def\nd@init{%
+ \let\open\nd@open%
+ \let\close\nd@close%
+ \let\hypo\nd@hypo%
+ \let\have\nd@have%
+ \let\hypocont\nd@hypocont%
+ \let\havecont\nd@havecont%
+ \let\by\nd@by%
+ \let\guard\nd@guard%
+ \csname\nd@rules\endcsname
+}
+
+% Define default rule names
+
+\def\ndrules{%
\def\ii{\by{$\Rightarrow$I}}%
\def\ie{\by{$\Rightarrow$E}}%
\def\Ai{\by{$\forall$I}}%
@@ -219,13 +282,34 @@
\def\ne{\by{$\neg$E}}%
\def\be{\by{$\bot$E}}%
\def\nne{\by{$\neg\neg$E}}%
- \def\r{\by{R}}%
-}
+ \def\r{\by{R}}}
+
+% default justification format
+
+\newcommand{\ndjustformat}[2]{#1, #2}
+
+% default line number format
+
+\newcommand{\ndrefformat}[1]{#1}
-\newenvironment{nd}{\begingroup\nd*init\nd*beginc}{\nd*endc\endgroup}
-\newenvironment{ndresume}{\begingroup\nd*init\nd*resumec}{\nd*endc\endgroup}
+% User-level commands for proofs
-\catcode`\*=\nd*astcode
+\newenvironment{nd}[1][]
+ {\begingroup
+ \setkeys{fitch}{#1}%
+ \nd@init\nd@beginc\ignorespaces}
+ {\nd@endc\endgroup}
+\newenvironment{ndresume}[1][]
+ {\begingroup
+ \setkeys{fitch}{#1}%
+ \nd@init\nd@resumec\ignorespaces}
+ {\nd@endc\endgroup}
+\newenvironment{fitchproof}[1][]
+ {\begin{list}{}{\setlength{\leftmargin}{0pt}}\item\begin{nd}[#1]}
+ {\end{nd}\end{list}}
+\newenvironment{fitchproof*}[1][]
+ {\begin{list}{}{\setlength{\leftmargin}{0pt}}\item\begin{ndresume}[#1]}
+ {\end{ndresume}\end{list}}
% End of file fitch.sty