Skip to content

Commit

Permalink
Add keyval options, fitchproof env, and change * to @
Browse files Browse the repository at this point in the history
  • Loading branch information
@rzach
rzach committed Sep 30, 2023
1 parent a7cb7f2 commit 24232d6
Show file tree
Hide file tree
Showing 3 changed files with 460 additions and 260 deletions.
5 changes: 5 additions & 0 deletions README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,11 @@ The output is shown above, and the corresponding LaTeX code below.

## Changes

**v1.0-alpha, Sept 30, 2023** This is an alpha release that adds key-value
options to the package and commands for customization. It is not fully
compatible with the 0.x versions (see documentation). Please report
any issues or suggestions.

**v0.6, Sept 4, 2023.** Updated the documentation and license (from
GPL to LPPL). The code is essentially unchanged.

Expand Down
316 changes: 190 additions & 126 deletions fitch.sty
View file
Original file line number Diff line number Diff line change
Expand Up @@ -50,159 +50,209 @@
% \]

\NeedsTeXFormat{LaTeX2e}
\ProvidesPackage{fitch}[2023-09-04 v0.6 Macros for Fitch-style natural deduction]
\ProvidesPackage{fitch}[2023-09-30 v1.0-alpha 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[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]

% 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,
height,
topheight,
depth,
labelsep,
indent,
hsep,
justsep,
linethickness,
cindent
}

\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{}
\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%
\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}
\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@t{\rule[-\nd@depth]{0mm}{\nd@height}\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@t}%
\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\gdef\nd@byt{\mbox{\csname\nd@justformat\endcsname{#1}{\ndref{#2}}}}\fi}

% 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}}
\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}}

% 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}}%
Expand All @@ -219,13 +269,27 @@
\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}

\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}
{\nd@endc\endgroup}
\newenvironment{fitchproof}
{\begin{list}{}{\setlength{\leftmargin}{0pt}}\item$\begin{nd}}
{\end{nd}$\end{list}}
% End of file fitch.sty
Loading

0 comments on commit 24232d6

Please sign in to comment.