summaryrefslogtreecommitdiff
path: root/macros/latex/contrib/fitch/fitch.hacker.txt
diff options
context:
space:
mode:
Diffstat (limited to 'macros/latex/contrib/fitch/fitch.hacker.txt')
-rw-r--r--macros/latex/contrib/fitch/fitch.hacker.txt256
1 files changed, 128 insertions, 128 deletions
diff --git a/macros/latex/contrib/fitch/fitch.hacker.txt b/macros/latex/contrib/fitch/fitch.hacker.txt
index df4af5c4da..9649a7b762 100644
--- a/macros/latex/contrib/fitch/fitch.hacker.txt
+++ b/macros/latex/contrib/fitch/fitch.hacker.txt
@@ -5,7 +5,7 @@ which is provided in the file fitchdoc.tex.
GENERAL
-Global identifiers defined by this package start with '\nd*'. The only
+Global identifiers defined by this package start with '\nd@'. The only
exceptions are \ndref, \nddim, \ndindent, and the "nd" and "ndresume"
latex environments.
@@ -22,36 +22,36 @@ REFERENCES
We start with some macros to facilitate automatic line numbering, and
for referencing of lines by labels. The macros defined here are:
-\nd*reset to reset the line number count. \nd*num{x}, to generate the
-next line number and store it in reference x; \nd*ref{x} to print the
+\nd@reset to reset the line number count. \nd@num{x}, to generate the
+next line number and store it in reference x; \nd@ref{x} to print the
line number referenced by x, \ndref{xxx} to parse a list of
references, separated by commas, periods, and hyphens, and translate
all references to line numbers. Note: \ndref ignores spaces in its
argument, but puts a space after each comma or period in the
-output. Also note: \nd*ref can be useful outside a natded environment,
+output. Also note: \nd@ref can be useful outside a natded environment,
and thus it has a user accessible name. Most general ``line numbers''
actually consist of a name (such as ``n'') and a number (such as
-``2''), to produce output such as $n+2$. \nd*set{n}{m} is called to
+``2''), to produce output such as $n+2$. \nd@set{n}{m} is called to
set the letter to n and the number to m. As special cases, if the
second argument is empty, it is not set, and if the first argument is
\relax, it is not set.
Example for references:
-\nd*reset \nd*num{x}; \nd*num{y}; \nd*numopt{n+1}{z}; \nd*num{zz};
-\nd*ref{y}; \ndref{x, y-zz, z}
+\nd@reset \nd@num{x}; \nd@num{y}; \nd@numopt{n+1}{z}; \nd@num{zz};
+\nd@ref{y}; \ndref{x, y-zz, z}
will produce: 1; 2; n+1; 3; 2; 1, 2-3, n+1
LAYER A
Layer A provides primitive picture elements which can be combined into
-natural deduction derivations. These are: \nd*t to make a topmost
-vertical line segment; \nd*v to make a continuation vertical line
-segment, \nd*i to produce the indentation for a subproof, \nd*s to
+natural deduction derivations. These are: \nd@t to make a topmost
+vertical line segment; \nd@v to make a continuation vertical line
+segment, \nd@i to produce the indentation for a subproof, \nd@s to
produce the horizontal space between a vertical line and a formula,
-\nd*u{x} to underline x with appropriate spacing for a
-hypothesis. \nd*f{x} typesets the formula x with the appropriate
-vertical spacing. \nd*g{x} is like \nd*i, except it puts a guard in
+\nd@u{x} to underline x with appropriate spacing for a
+hypothesis. \nd@f{x} typesets the formula x with the appropriate
+vertical spacing. \nd@g{x} is like \nd@i, except it puts a guard in
the space it creates. These elements are spaced so that they are
appropriate as left-aligned array entries. Line numberings and
justifications must be provided manually in this layer. All explicit
@@ -62,91 +62,91 @@ Example of a derivation using layer A syntax:
\[
\begin{array}{lll}
- 1 & \nd*t\nd*s\nd*f {P\vee Q} \\
- 2 & \nd*v\nd*s\nd*u {\neg Q} \\
- 3 & \nd*v\nd*i\nd*t\nd*s\nd*u {P} \\
- 4 & \nd*v\nd*i\nd*v\nd*s\nd*f {P} & \mbox{by 3} \\
- 5 & \nd*v\nd*i\nd*t\nd*s\nd*u {Q} \\
- 6 & \nd*v\nd*i\nd*v\nd*s\nd*f {\neg Q} & \mbox{by 2} \\
- 7 & \nd*v\nd*i\nd*v\nd*s\nd*f {\bot} & \mbox{by 5, 6} \\
- 8 & \nd*v\nd*i\nd*v\nd*s\nd*f {P} & \mbox{by 7} \\
- 9 & \nd*v\nd*s\nd*f {P} & \mbox{by 1, 3-4, 5-8} \\
+ 1 & \nd@t\nd@s\nd@f {P\vee Q} \\
+ 2 & \nd@v\nd@s\nd@u {\neg Q} \\
+ 3 & \nd@v\nd@i\nd@t\nd@s\nd@u {P} \\
+ 4 & \nd@v\nd@i\nd@v\nd@s\nd@f {P} & \mbox{by 3} \\
+ 5 & \nd@v\nd@i\nd@t\nd@s\nd@u {Q} \\
+ 6 & \nd@v\nd@i\nd@v\nd@s\nd@f {\neg Q} & \mbox{by 2} \\
+ 7 & \nd@v\nd@i\nd@v\nd@s\nd@f {\bot} & \mbox{by 5, 6} \\
+ 8 & \nd@v\nd@i\nd@v\nd@s\nd@f {P} & \mbox{by 7} \\
+ 9 & \nd@v\nd@s\nd@f {P} & \mbox{by 1, 3-4, 5-8} \\
\end{array}
\]
LISTS
This is a bit of a hack. We implement linked lists as follows: a list
-is either \nd*nil, or \nd*cons{T}{H}, where T is another list, and H
+is either \nd@nil, or \nd@cons{T}{H}, where T is another list, and H
is some arbitrary code. Note that lists grow to the right. The
following macros operate on a list that is stored in a macro \list.
-\nd*push\list{item} pushes the item onto the list
-\nd*pop\list{item} pops and discards the last item from the list
-\nd*item\list{command} applies command to each element of the list
-\nd*modify\list\n{elt} modifies the \n-th element of the
+\nd@push\list{item} pushes the item onto the list
+\nd@pop\list{item} pops and discards the last item from the list
+\nd@item\list{command} applies command to each element of the list
+\nd@modify\list\n{elt} modifies the \n-th element of the
list, if there is such an element. Here \n is a counter. Elements
are counted from the right, starting from 1.
-We use lists of items of the forms \nd*t, \nd*v, \nd*i, and \nd*g{...}
+We use lists of items of the forms \nd@t, \nd@v, \nd@i, and \nd@g{...}
to represent the current indentation level and format (see Layer A,
-above). The function \nd*cont computes the indentation for the
-following line by replacing all items of the form \nd*t by \nd*v and
-\nd*g{...} by \nd*i.
+above). The function \nd@cont computes the indentation for the
+following line by replacing all items of the form \nd@t by \nd@v and
+\nd@g{...} by \nd@i.
With the list syntax, a derivation can be expressed like this:
\[
\begin{array}{lll}
- \gdef\stack{\nd*nil}
+ \gdef\stack{\nd@nil}
\newcount\n
- \nd*push\stack{\nd*t}
- 1 & \nd*iter\stack\relax\nd*s\nd*u {\neg\exists xP(x)} \\
- \nd*cont\stack
- \nd*push\stack{\nd*i}
- \nd*push\stack{\nd*t}
- \nd*n=2\nd*modify\stack\n{\nd*g{u}}
- \nd*push\stack{\nd*i}
- \nd*push\stack{\nd*t}
- 2 & \nd*iter\stack\relax\nd*s\nd*u {P(u)} \\
- \nd*cont\stack
- 3 & \nd*iter\stack\relax\nd*s\nd*f {\exists xP(x)} \\
- \nd*cont\stack
- 4 & \nd*iter\stack\relax\nd*s\nd*f {\neg\exists xP(x)} \\
- \nd*cont\stack
- 5 & \nd*iter\stack\relax\nd*s\nd*f {\bot} \\
- \nd*cont\stack
- \nd*pop\stack
- \nd*pop\stack
- 6 & \nd*iter\stack\relax\nd*s\nd*f {\neg P(u)} \\
- \nd*cont\stack
- \nd*pop\stack
- \nd*pop\stack
- 7 & \nd*iter\stack\relax\nd*s\nd*f {\forall y\neg P(y)} \\
- \nd*cont\stack
+ \nd@push\stack{\nd@t}
+ 1 & \nd@iter\stack\relax\nd@s\nd@u {\neg\exists xP(x)} \\
+ \nd@cont\stack
+ \nd@push\stack{\nd@i}
+ \nd@push\stack{\nd@t}
+ \nd@n=2\nd@modify\stack\n{\nd@g{u}}
+ \nd@push\stack{\nd@i}
+ \nd@push\stack{\nd@t}
+ 2 & \nd@iter\stack\relax\nd@s\nd@u {P(u)} \\
+ \nd@cont\stack
+ 3 & \nd@iter\stack\relax\nd@s\nd@f {\exists xP(x)} \\
+ \nd@cont\stack
+ 4 & \nd@iter\stack\relax\nd@s\nd@f {\neg\exists xP(x)} \\
+ \nd@cont\stack
+ 5 & \nd@iter\stack\relax\nd@s\nd@f {\bot} \\
+ \nd@cont\stack
+ \nd@pop\stack
+ \nd@pop\stack
+ 6 & \nd@iter\stack\relax\nd@s\nd@f {\neg P(u)} \\
+ \nd@cont\stack
+ \nd@pop\stack
+ \nd@pop\stack
+ 7 & \nd@iter\stack\relax\nd@s\nd@f {\forall y\neg P(y)} \\
+ \nd@cont\stack
\end{array}
\]
LAYER B
Layer B is simply a wrapper around layer A. It provides commands
-\nd*beginb, \nd*resumeb, \nd*endb, \nd*openb, \nd*closeb, \nd*guardb,
-\nd*hypob, and \nd*haveb which abstract from the layer A
+\nd@beginb, \nd@resumeb, \nd@endb, \nd@openb, \nd@closeb, \nd@guardb,
+\nd@hypob, and \nd@haveb which abstract from the layer A
primitives. This includes automatic line numbering, and automatic
-indentation. \nd*hypocontb and \nd*havecontb are like \nd*hypob and
-\nd*haveb, except that they introduce continuation lines that are
-slightly indented and have no line number/label. \nd*beginb and
-\nd*endb enclose a natural deduction in layer B syntax. \nd*resumeb is
-like \nd*beginb, except that it resumes a deduction in progress (for
-instance, after a manual page break). \nd*openb and \nd*closeb open,
-respectively close, a subproof. \nd*guardb{n}{g} adds the guard g to
+indentation. \nd@hypocontb and \nd@havecontb are like \nd@hypob and
+\nd@haveb, except that they introduce continuation lines that are
+slightly indented and have no line number/label. \nd@beginb and
+\nd@endb enclose a natural deduction in layer B syntax. \nd@resumeb is
+like \nd@beginb, except that it resumes a deduction in progress (for
+instance, after a manual page break). \nd@openb and \nd@closeb open,
+respectively close, a subproof. \nd@guardb{n}{g} adds the guard g to
the nth enclosing subderivation (counted from 1 from the
-inside). \nd*hypob introduces a hypothesis, and \nd*haveb introduces a
+inside). \nd@hypob introduces a hypothesis, and \nd@haveb introduces a
non-hypothesis line in a proof. Line numbering is integrated, but
justifications must still be given manually. Also, proof lines must
still be terminated by '\\'. An idiosyncracy of this layer is that in
a list of several hypotheses, all but the last one must be called with
-\nd*haveb, not \nd*hypob, to avoid drawing a horizontal line under
+\nd@haveb, not \nd@hypob, to avoid drawing a horizontal line under
each of them.
Example of a derivation using layer B syntax. Note that the "line
@@ -154,40 +154,40 @@ numbers" are really labels, which will be replaced by consecutive line
numbers in the output.
\[
- \nd*beginb
- \nd*haveb {1}{P\vee Q} \\
- \nd*hypob {2}{\neg Q} \\
- \nd*openb
- \nd*hypob {3}{P} \\
- \nd*haveb {4}{P} \mbox{by \ndref{3}} \\
- \nd*closeb
- \nd*openb
- \nd*hypob {5}{Q} \\
- \nd*haveb {6}{\neg Q} \mbox{by \ndref{2}} \\
- \nd*haveb {6a}{\bot} \mbox{by \ndref{5,6}} \\
- \nd*haveb {6b}{P} \mbox{by \ndref{6a}} \\
- \nd*closeb
- \nd*haveb {8}{P} \mbox{by \ndref{1,3-4,5-6b}} \\
- \nd*endb
+ \nd@beginb
+ \nd@haveb {1}{P\vee Q} \\
+ \nd@hypob {2}{\neg Q} \\
+ \nd@openb
+ \nd@hypob {3}{P} \\
+ \nd@haveb {4}{P} \mbox{by \ndref{3}} \\
+ \nd@closeb
+ \nd@openb
+ \nd@hypob {5}{Q} \\
+ \nd@haveb {6}{\neg Q} \mbox{by \ndref{2}} \\
+ \nd@haveb {6a}{\bot} \mbox{by \ndref{5,6}} \\
+ \nd@haveb {6b}{P} \mbox{by \ndref{6a}} \\
+ \nd@closeb
+ \nd@haveb {8}{P} \mbox{by \ndref{1,3-4,5-6b}} \\
+ \nd@endb
\]
Here is another example, using a guard.
\[
- \nd*beginb
- \nd*hypob {1}{\neg\exists xP(x)} \\
- \nd*openb
- \nd*guardb {1}{u}
- \nd*openb
- \nd*hypob {2}{P(u)} \\
- \nd*haveb {3}{\exists xP(x)} \mbox{by \ndref{2}} \\
- \nd*haveb {4}{\neg\exists xP(x)} \mbox{by \ndref{1}} \\
- \nd*haveb {5}{\bot} \mbox{by \ndref{3,4}}\\
- \nd*closeb
- \nd*haveb {6}{\neg P(u)} \mbox{by \ndref{2-5}}\\
- \nd*closeb
- \nd*haveb {7}{\forall y\neg P(y)} \mbox{by \ndref{2-6}}\\
- \nd*endb
+ \nd@beginb
+ \nd@hypob {1}{\neg\exists xP(x)} \\
+ \nd@openb
+ \nd@guardb {1}{u}
+ \nd@openb
+ \nd@hypob {2}{P(u)} \\
+ \nd@haveb {3}{\exists xP(x)} \mbox{by \ndref{2}} \\
+ \nd@haveb {4}{\neg\exists xP(x)} \mbox{by \ndref{1}} \\
+ \nd@haveb {5}{\bot} \mbox{by \ndref{3,4}}\\
+ \nd@closeb
+ \nd@haveb {6}{\neg P(u)} \mbox{by \ndref{2-5}}\\
+ \nd@closeb
+ \nd@haveb {7}{\forall y\neg P(y)} \mbox{by \ndref{2-6}}\\
+ \nd@endb
\]
LAYER C
@@ -197,42 +197,42 @@ information and putting it correctly into an array. Specifically, in
layer C, it is no more necessary to explicitly give '\\', and all
hypotheses are denoted \hypo. Layer C also provides a convenient
syntax for writing justification labels. Further, layer C provides
-``multi-line'' commands, thus e.g. \nd*mhypoc{a}{x\\y\\z} is an
-abbreviation for \nd*hypoc{a}{x}\nd*hypocontc{y}\nd*hypocontc{z}. In
-addition there is a \nd*by command for writing justification labels,
-in the style of \nd*by{$\vee$E}{1,2-4,5-6}.
+``multi-line'' commands, thus e.g. \nd@mhypoc{a}{x\\y\\z} is an
+abbreviation for \nd@hypoc{a}{x}\nd@hypocontc{y}\nd@hypocontc{z}. In
+addition there is a \nd@by command for writing justification labels,
+in the style of \nd@by{$\vee$E}{1,2-4,5-6}.
-Commands exported by layer C are: \nd*hypoc, \nd*havec, \nd*hypocontc,
-\nd*havecontc, \nd*mhypoc, \nd*mhavec, \nd*mhypocontc, \nd*mhavecontc,
-\nd*by, \nd*beginc, \nd*resumec, \nd*endc, \nd*openc, \nd*closec,
-\nd*guardc.
+Commands exported by layer C are: \nd@hypoc, \nd@havec, \nd@hypocontc,
+\nd@havecontc, \nd@mhypoc, \nd@mhavec, \nd@mhypocontc, \nd@mhavecontc,
+\nd@by, \nd@beginc, \nd@resumec, \nd@endc, \nd@openc, \nd@closec,
+\nd@guardc.
The layer C macros work by storing each line in a data structure
-\ppp,\nd*typ,\nd*byt. The line is ejected when the beginning of the
+\ppp,\nd@typ,\nd@byt. The line is ejected when the beginning of the
next line is read, and once at the very end. In this way, we can put
in the correct line breaks (whether or not the line carries a
justification), and a hypothesis does not get typeset until we know
-whether it is followed by another hypothesis. \nd*sto stores a new
-line, \nd*clr clears the current line, \nd*cmd outputs the current
+whether it is followed by another hypothesis. \nd@sto stores a new
+line, \nd@clr clears the current line, \nd@cmd outputs the current
line.
Example of layer C syntax:
\[
- \nd*beginc
- \nd*hypoc {1}{\neg\exists xP(x)}
- \nd*openc
- \nd*guardc {1}{u}
- \nd*openc
- \nd*hypoc {2}{P(u)}
- \nd*havec {3}{\exists xP(x)} \nd*by{$\exists$I}{2}
- \nd*havec {4}{\neg\exists xP(x)} \nd*by{R}{1}
- \nd*havec {5}{\bot} \nd*by{$\neg$E}{3,4}
- \nd*closec
- \nd*havec {6}{\neg P(u)} \nd*by{$\neg$I}{2-5}
- \nd*closec
- \nd*havec {7}{\forall y\neg P(y)} \nd*by{$\forall$I}{2-6}
- \nd*endc
+ \nd@beginc
+ \nd@hypoc {1}{\neg\exists xP(x)}
+ \nd@openc
+ \nd@guardc {1}{u}
+ \nd@openc
+ \nd@hypoc {2}{P(u)}
+ \nd@havec {3}{\exists xP(x)} \nd@by{$\exists$I}{2}
+ \nd@havec {4}{\neg\exists xP(x)} \nd@by{R}{1}
+ \nd@havec {5}{\bot} \nd@by{$\neg$E}{3,4}
+ \nd@closec
+ \nd@havec {6}{\neg P(u)} \nd@by{$\neg$I}{2-5}
+ \nd@closec
+ \nd@havec {7}{\forall y\neg P(y)} \nd@by{$\forall$I}{2-6}
+ \nd@endc
\]
LAYER D
@@ -250,24 +250,24 @@ global name space. There is also an environment ndresume which is like
nd, except that it continues a proof in progress (with continuous
nesting and labeling).
-The macros \nd*hypod, \nd*haved, \nd*opend, \nd*guardd are essentially
+The macros \nd@hypod, \nd@haved, \nd@opend, \nd@guardd are essentially
the user-level macros, but with all optional argument spelled-out. The
versions without the final "d" allow the optional arguments to be
omitted.
-The functions \nd*optarg and \nd*optargg are used to handle optional
-arguments. Usage: \nd*optarg{default}{continuation}xxx - reads an
+The functions \nd@optarg and \nd@optargg are used to handle optional
+arguments. Usage: \nd@optarg{default}{continuation}xxx - reads an
optional argument, supplies default if necessary, then continues with
continuation. Continuation expects optional argument between
-[...]. I.e., \nd*optarg{d}{c}[xxx] => c[xxx], and \nd*optarg{d}{c}x =>
-c[d]x if x != '['. Behavior is undefined if x is {[...}. \nd*optargg
+[...]. I.e., \nd@optarg{d}{c}[xxx] => c[xxx], and \nd@optarg{d}{c}x =>
+c[d]x if x != '['. Behavior is undefined if x is {[...}. \nd@optargg
is similar except it takes two continuations: first one for optional
argument present, second for not present. It takes no default value.
-The function \nd*five{\a} reads five, partly optional arguments of the
+The function \nd@five{\a} reads five, partly optional arguments of the
shape [][]{}[]{}, then call \a with these arguments.
-Finally, \nd*init puts all the commands which are visible inside an
+Finally, \nd@init puts all the commands which are visible inside an
nd-environment in the current name space.
Example of a derivation using layer D syntax. As before, the "line