Skip to content

Commit 759722d

Browse files
committed
describe special features of package already on first page of manual
1 parent ea31749 commit 759722d

1 file changed

Lines changed: 15 additions & 8 deletions

File tree

fitchdoc.tex

Lines changed: 15 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -89,12 +89,20 @@ \section{Overview}
8989
\end{LTXexample}
9090

9191
A derivation consists of \emph{lines}, and each line contains a {\em
92-
line number} and a \emph{formula}. Some lines also carry a {\em
92+
line label} and a \emph{formula}. Some lines also carry a {\em
9393
justification}. Moreover, each line is either a \emph{hypothesis} or a
94-
\emph{derived formula}. Generally, derived formulas carry a
94+
\emph{derived formula}. Usually, derived formulas carry a
9595
justification, whereas hypotheses do not; however, the macros do not
9696
enforce this.
9797

98+
Proofs set using |fitch.sty| will have lines numbered automatically in
99+
the output. It is possible to override the automatic numbering (see
100+
Section~\ref{subsec-customline}). You can refer to line numbers in the
101+
text using |\ndref| (see Section~\ref{subsec-ndref}). Various
102+
dimensions, formatting of justifications and line references, and the
103+
shorthand macros used to produce rule names can be customized (see
104+
Section~\ref{sec-customization}).
105+
98106
\section{Usage}\label{sec-usage}
99107

100108
\DescribeEnv{nd}\DescribeEnv{fitchproof} Derivations are typeset
@@ -232,16 +240,15 @@ \subsection{Generic justifications}
232240
In the default justification format, a comma is automatically inserted
233241
between the name and the reference list, unless the reference list is
234242
empty. The formatting of justifications can be changed, see
235-
Section~\ref{sec-customization}. If the reference list is empty, only
236-
the first argument (without formatting or punctuation) is printed.
237-
\NewIn{1.0} If
238-
the first argument is empty, only the reference list is printed.
243+
Section~\ref{sec-customization}. If the second argument (the reference
244+
list) is empty, only the first argument (without formatting or
245+
punctuation) is printed. \NewIn{1.0} If the first argument is empty,
246+
only the reference list is printed.
239247
240248
Since the |\by| command outputs its first argument without additional
241249
formatting when the second argument is empty, you can use |\by{...}{}|
242250
to produce arbitrary text in the justification. You can use the
243-
|\ndref| command here. If the first argument is empty, only the
244-
reference list is printed.
251+
|\ndref| command here.
245252
\begin{LTXexample}
246253
$
247254
\begin{nd}

0 commit comments

Comments
 (0)