texlive[68179] Master: fitch (5sep23)
commits+karl at tug.org
commits+karl at tug.org
Tue Sep 5 22:05:12 CEST 2023
Revision: 68179
http://tug.org/svn/texlive?view=revision&revision=68179
Author: karl
Date: 2023-09-05 22:05:11 +0200 (Tue, 05 Sep 2023)
Log Message:
-----------
fitch (5sep23)
Modified Paths:
--------------
trunk/Master/tlpkg/bin/tlpkg-ctan-check
trunk/Master/tlpkg/tlpsrc/collection-mathscience.tlpsrc
Added Paths:
-----------
trunk/Master/texmf-dist/doc/latex/fitch/
trunk/Master/texmf-dist/doc/latex/fitch/README.md
trunk/Master/texmf-dist/doc/latex/fitch/fitch.hacker.txt
trunk/Master/texmf-dist/doc/latex/fitch/fitchdoc-dimen.pdf
trunk/Master/texmf-dist/doc/latex/fitch/fitchdoc.pdf
trunk/Master/texmf-dist/doc/latex/fitch/fitchdoc.tex
trunk/Master/texmf-dist/doc/latex/fitch/fitchexample.png
trunk/Master/texmf-dist/tex/latex/fitch/
trunk/Master/texmf-dist/tex/latex/fitch/fitch.sty
trunk/Master/tlpkg/tlpsrc/fitch.tlpsrc
Added: trunk/Master/texmf-dist/doc/latex/fitch/README.md
===================================================================
--- trunk/Master/texmf-dist/doc/latex/fitch/README.md (rev 0)
+++ trunk/Master/texmf-dist/doc/latex/fitch/README.md 2023-09-05 20:05:11 UTC (rev 68179)
@@ -0,0 +1,82 @@
+# fitch.sty
+
+LaTeX macros for Fitch style natural deduction
+
+## Usage
+
+Fitch-style natural deduction is a system for writing proofs in
+propositional logic and predicate logic. This is a set of easy-to-use
+LaTeX macros originally written by Peter Selinger. It is used, e.g.,
+in the various versions of _forall x_ by PD Magnus (e.g., the [original](https://www.fecundity.com/logic/download.html),
+[Cambridge](http://www.homepages.ucl.ac.uk/~uctytbu/OERs.html), and [Calgary](https://forallx.openlogicproject.org) versions)
+
+With these macros, one can typeset natural deduction proofs in Fitch
+style, as in the following example:
+
+
+
+```
+\begin{nd}
+ \hypo {1} {\forall y \neg P(y)}
+ \open
+ \hypo {2} {\exists x P(x)}
+ \open[u]
+ \hypo {3} {P(u)}
+ \have {4}{\forall y \neg P(y)} \r{1}
+ \have {5} {\neg P(u)} \Ae{4}
+ \have {6} {\bot} \ne{3,5}
+ \close
+ \have {6a} {\bot} \Ee{2,3-6}
+ \close
+ \have {7} {\neg \exists x P(x)} \ni{2-6a}
+\end{nd}
+```
+
+The output is shown above, and the corresponding LaTeX code below.
+
+## Changes
+
+**v0.6, Sept 4, 2023.** Updated the documentation and license (from
+GPL to LPPL). The code is essentially unchanged.
+
+**v0.5, Feb 8, 2005.** The ability to handle multi-line formulas
+was added.
+
+## Download
+
+The package is available on CTAN as
+[`fitch`](https://ctan.org/pkg/fitch).
+
+The code is [maintained on Github](https://github.com/OpenLogicProject/fitch/).
+
+## Related packages
+
+- The [`lplfitch`](https://ctan.org/pkg/lplfitch) packages produces
+ Fitch-style roofs in the format used in Barwise & Etchemendy's textbook
+ _Language, Proof, and Logic_.
+- The [`natded`](https://ctan.org/pkg/natded) package produces natural
+ deduction roofs in the style of Jaśkowski, or that of Kalish and
+ Montague.
+
+Additional packages for proofs, including Johan Klüwer's, are
+available at a [page maintained by Alex Kocurek](https://www.actual.world/latex/)
+
+## People
+
+Peter Selinger, Dalhousie University, is the original author.
+
+Richard Zach, University of Calgary, it the current maintainer.
+
+## License
+
+Copyright (C) 2002-2023 Peter Selinger
+
+This work may be distributed and/or modified under the conditions of
+the LaTeX Project Public License, either version 1.3 of this license
+or (at your option) any later version. The latest version of this
+license is in
+
+ https://www.latex-project.org/lppl.txt
+
+and version 1.3c or later is part of all distributions of LaTeX
+version 2008 or later.
\ No newline at end of file
Property changes on: trunk/Master/texmf-dist/doc/latex/fitch/README.md
___________________________________________________________________
Added: svn:eol-style
## -0,0 +1 ##
+native
\ No newline at end of property
Added: trunk/Master/texmf-dist/doc/latex/fitch/fitch.hacker.txt
===================================================================
--- trunk/Master/texmf-dist/doc/latex/fitch/fitch.hacker.txt (rev 0)
+++ trunk/Master/texmf-dist/doc/latex/fitch/fitch.hacker.txt 2023-09-05 20:05:11 UTC (rev 68179)
@@ -0,0 +1,314 @@
+This file describes the internals of the macros in fitch.sty. It is
+intended for programmers who might want to hack this package. For
+information on how to use the package, please see the user guide,
+which is provided in the file fitchdoc.tex.
+
+GENERAL
+
+Global identifiers defined by this package start with '\nd*'. The only
+exceptions are \ndref, \nddim, \ndindent, and the "nd" and "ndresume"
+latex environments.
+
+The macros provided by this package mix TeX and LaTeX primitives.
+LaTeX is used for \rule, \settowidth, \addtolength, \hspace... All
+macros are assumed to be called in math mode.
+
+Translation proceeds through several layers of macros. Each layer
+consist of macros which expand into macros of the previous layer. Each
+layer may have some global state and initialization functions. Only
+the topmost layer (layer D) is directly user-accessible.
+
+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
+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,
+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
+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}
+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
+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
+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
+spacing information is contained in this layer; higher layers
+manipulate only layer A primitives.
+
+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} \\
+\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 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
+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{...}
+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.
+
+With the list syntax, a derivation can be expressed like this:
+
+\[
+\begin{array}{lll}
+ \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
+\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
+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
+the nth enclosing subderivation (counted from 1 from the
+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
+each of them.
+
+Example of a derivation using layer B syntax. Note that the "line
+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
+\]
+
+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
+\]
+
+LAYER C
+
+Layer C is a wrapper around layer B. It takes care of buffering
+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}.
+
+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
+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
+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
+\]
+
+LAYER D
+
+Layer D is the syntax used by the end user. It is implemented as a
+wrapper around layer C, providing three additional conveniences: (1) a
+latex environment, (2) guard as optional argument to \have, \hypo, or
+\open, (3) optional relabeling arguments. The user level commands are
+similar to those of layer C: they are called \begin{nd}, \end{nd},
+\open, \close, \hypo, \have, \guard, \by. For convenience, a number
+of abbreviations are also provided for writing justifications. For
+instance \ie for \by{$\Rightarrow$E} etc. These commands are only
+visible inside an nd-environment; thus they do not interfere with the
+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 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
+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
+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
+shape [][]{}[]{}, then call \a with these arguments.
+
+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
+numbers" are really labels, which will be replaced by consecutive line
+numbers in the output.
+
+\[
+\begin{nd}
+ \hypo{1} {P\vee Q}
+ \hypo{2} {\neg Q}
+ \open
+ \hypo{3a} {P}
+ \have{3b} {P} \r{3a}
+ \close
+ \open
+ \hypo{4a} {Q}
+ \have{4b} {\neg Q} \r{2}
+ \have{4c} {\bot} \ne{4a,4b}
+ \have{4d} {P} \be{4c}
+ \close
+ \have{5} {P} \oe{1,3a-3b,4a-4d}
+\end{nd}
+\]
+
+Another example of layer D syntax, using guards and relabelings:
+
+\[
+\begin{nd}
+ \hypo {1} {P\vee Q}
+ \open[u]
+ \hypo {2} {P}
+ \have [\vdots] {3} {\vdots}
+ \have [n][-1] {4} {A\wedge B}
+ \close
+ \open
+ \hypo {5} {Q}
+ \have [\vdots] {6} {\vdots}
+ \have [m] {7} {A\wedge B}
+ \close
+ \have {8} {A\wedge B} \oe{1,2-(4),5-7}
+ \have [\vdots] {9} {\vdots}
+ \have [][100] {10} {A} \ae{8}
+\end{nd}
+\]
Property changes on: trunk/Master/texmf-dist/doc/latex/fitch/fitch.hacker.txt
___________________________________________________________________
Added: svn:eol-style
## -0,0 +1 ##
+native
\ No newline at end of property
Added: trunk/Master/texmf-dist/doc/latex/fitch/fitchdoc-dimen.pdf
===================================================================
(Binary files differ)
Index: trunk/Master/texmf-dist/doc/latex/fitch/fitchdoc-dimen.pdf
===================================================================
--- trunk/Master/texmf-dist/doc/latex/fitch/fitchdoc-dimen.pdf 2023-09-04 23:43:36 UTC (rev 68178)
+++ trunk/Master/texmf-dist/doc/latex/fitch/fitchdoc-dimen.pdf 2023-09-05 20:05:11 UTC (rev 68179)
Property changes on: trunk/Master/texmf-dist/doc/latex/fitch/fitchdoc-dimen.pdf
___________________________________________________________________
Added: svn:mime-type
## -0,0 +1 ##
+application/pdf
\ No newline at end of property
Added: trunk/Master/texmf-dist/doc/latex/fitch/fitchdoc.pdf
===================================================================
(Binary files differ)
Index: trunk/Master/texmf-dist/doc/latex/fitch/fitchdoc.pdf
===================================================================
--- trunk/Master/texmf-dist/doc/latex/fitch/fitchdoc.pdf 2023-09-04 23:43:36 UTC (rev 68178)
+++ trunk/Master/texmf-dist/doc/latex/fitch/fitchdoc.pdf 2023-09-05 20:05:11 UTC (rev 68179)
Property changes on: trunk/Master/texmf-dist/doc/latex/fitch/fitchdoc.pdf
___________________________________________________________________
Added: svn:mime-type
## -0,0 +1 ##
+application/pdf
\ No newline at end of property
Added: trunk/Master/texmf-dist/doc/latex/fitch/fitchdoc.tex
===================================================================
--- trunk/Master/texmf-dist/doc/latex/fitch/fitchdoc.tex (rev 0)
+++ trunk/Master/texmf-dist/doc/latex/fitch/fitchdoc.tex 2023-09-05 20:05:11 UTC (rev 68179)
@@ -0,0 +1,406 @@
+%% fitchdoc.tex
+%% Macros for Fitch-style natural deduction (documentation)
+%% Copyright 2002-2023 Peter Selinger
+%
+% This work may be distributed and/or modified under the
+% conditions of the LaTeX Project Public License, either version 1.3
+% of this license or (at your option) any later version.
+% The latest version of this license is in
+% https://www.latex-project.org/lppl.txt
+% and version 1.3c or later is part of all distributions of LaTeX
+% version 2008 or later.
+%
+% This work has the LPPL maintenance status `maintained'.
+%
+% The Current Maintainer of this work is Richard Zach <rzach at ucalgary.ca>
+%
+% This work consists of the files fitch.sty and fitchdoc.tex.
+
+% Original Author: Peter Selinger, Dalhousie University
+% Created: Jan 14, 2002
+% Modified: Sep 4, 2023
+% Version: 0.6
+% Copyright: (C) 2002-2023 Peter Selinger
+% Filename: fitch.sty
+% Documentation: fitchdoc.tex
+% https://github.com/OpenLogicProject/fitch/
+
+\documentclass{ltxdoc}
+
+\usepackage{fitch,graphicx,showexpl,fullpage}
+
+\lstset{%
+ basicstyle=\ttfamily\small,
+ commentstyle=\itshape\ttfamily\small,
+ showspaces=false,
+ showstringspaces=false,
+ breaklines=true,
+ breakautoindent=true,
+ captionpos=t
+}
+
+\title{\texttt{fitch.sty}: Fitch-style natural deduction macros}
+
+\author{Peter Selinger\\Dalhousie University\thanks{The current
+maintainer of this package is \href{https://richardzach.org}{Richard
+Zach}. The package repository is at
+\url{https://github.com/OpenLogicProject/fitch/}, where you can also
+report any \href{https://github.com/OpenLogicProject/fitch/issues}{issues} with it.}}
+
+\date{Version 0.6\\ September 4, 2023}
+
+\begin{document}
+\maketitle
+
+\section{Overview}
+
+This document describes how to use the {\tt fitch.sty} macros for
+typesetting Fitch-style natural deduction derivations. To load the macros,
+simply put \verb!\usepackage{fitch}! into the preamble of your
+{\LaTeX} file.
+
+Here is a natural deduction derivation, together with the code that
+produced it:
+
+\begin{LTXexample}
+\[
+\begin{nd}
+ \hypo {1} {P\vee Q}
+ \hypo {2} {\neg Q}
+ \open
+ \hypo {3} {P}
+ \have {4} {P} \r{3}
+ \close
+ \open
+ \hypo {aa} {Q}
+ \have {6} {\neg Q} \r{2}
+ \have {7} {\bot} \ne{aa,6}
+ \have {8} {P} \be{7}
+ \close
+ \have {9} {P} \oe{1,3-4,aa-8}
+\end{nd}
+\]
+\end{LTXexample}
+
+A derivation consists of \emph{lines}, and each line contains a {\em
+line number} and a \emph{formula}. Some lines also carry a {\em
+justification}. Moreover, each line is either a \emph{hypothesis} or a
+\emph{derived formula}. Generally, derived formulas carry a
+justification, whereas hypotheses do not; however, the macros do not
+enforce this.
+
+\DescribeEnv{nd}
+Derivations are typeset inside the \verb!nd! environment, which must be
+used in math mode.
+
+\DescribeMacro{\hypo}\DescribeMacro{\have}
+The commands \verb!\hypo! and \verb!\have! are used
+to typeset one line of the derivation; \verb!\hypo! is used for
+hypotheses, and \verb!\have! for derived formulas. Both commands take
+a label and a formula as an argument. Note that the labels used to
+identify lines in the derivation need not be actual line numbers; for
+instance, in the above example, we used the label $aa$ instead of $5$.
+In the output, lines are automatically numbered consecutively. Labels
+may not contain any punctuation characters or spaces.
+
+\DescribeMacro{\open}\DescribeMacro{\close}
+Subderivations are opened and closed with the commands \verb!\open! and
+\verb!\close!. Finally, the following commands are provided for
+annotating lines with justifications:
+
+\medskip
+\hfill
+\begin{tabular}{@{}ll@{}}
+ \verb!\r! & reiteration \\
+ \verb!\ii! & implication introduction \\
+ \verb!\ie! & implication elimination \\
+ \verb!\ai! & and introduction \\
+ \verb!\ae! & and elimination \\
+\end{tabular}
+\hfill
+\begin{tabular}{ll}
+ \verb!\oi! & or introduction \\
+ \verb!\oe! & or elimination \\
+ \verb!\ni! & not introduction \\
+ \verb!\ne! & not elimination \\
+ \verb!\be! & bottom elimination \\
+\end{tabular}
+\hfill
+\begin{tabular}{@{}ll@{}}
+ \verb!\nne! & double negation elimination \\
+ \verb!\Ai! & forall introduction \\
+ \verb!\Ae! & forall elimination \\
+ \verb!\Ei! & exists introduction \\
+ \verb!\Ee! & exists elimination \\
+\end{tabular}
+\hfill
+\medskip
+
+Each such command takes a \emph{reference list} as an argument. A
+reference list is a string made from labels, commas, and hyphens, for
+instance \verb!1,3a-3b,4a-4d!.
+
+\section{Details}
+
+\subsection{Guards}
+
+Some natural deduction derivations with quantifiers use \emph{guards}, as in
+the following example:
+
+\begin{LTXexample}
+\[
+\begin{nd}
+ \hypo {1} {\exists x\forall y.P(x,y)}
+ \open[v]
+ \open[u]
+ \hypo {2} {\forall y.P(u,y)}
+ \have {3} {P(u,v)} \Ae{2}
+ \have {4} {\exists x.P(x,v)} \Ei{3}
+ \close
+ \have {5} {\exists x.P(x,v)} \Ee{1,2-5}
+ \close
+ \have {6} {\forall y\exists x.P(x,y)} \Ai{2-5}
+\end{nd}
+\]
+\end{LTXexample}
+
+The guards $v$ and $u$ in line 2 were typeset by giving optional
+arguments to the \verb!\open! commands of the respective
+subderivations.
+
+\DescribeMacro{\guard}
+For most purposes, the above way of specifying guards is sufficient.
+However, there is another method, which allows a more flexible
+placement of guards: before any line, you can give the command
+\verb!\guard{u}! to add a guard $u$ to the top-level subderivation at
+that line, or \verb!\guard[n]{u}! to add a guard to the $n$th
+enclosing subderivation at that line. Thus, the above example could
+have also been typeset by inserting the two commands \verb!\guard{u}! and
+\verb!\guard[2]{v}! just after the second \verb!\open! statement.
+
+% For backward compatibility, there is a third way of specifying guards
+% by giving an optional second argument to the \verb!\hypo! and
+% \verb!\have! commands. The use of this feature is discouraged.
+
+\subsection{Generic justifications}
+
+Non-standard justifications can be created with the \verb!\by!
+command. This command takes two arguments: a name and a reference
+list. For instance, the command \verb!\by{De Morgan}{lab3,lab4}! might
+produce the output ``\mbox{De Morgan, 3, 4}''. Note that the justification
+is typeset in text mode. A comma is automatically inserted between the
+name and the reference list, unless the reference list is empty.
+
+\subsection{Label and reference list details}
+
+Labels may not contain commas, periods, semicolons, hyphens,
+parenthesis, or spaces. In a reference list, spaces are ignored (even
+within a label!), whereas commas, periods, semicolons, parenthesis,
+and hyphens are copied to the output. All other characters are
+interpreted as part of a label. Attempting to reference a label which
+has not been previously defined by any \verb!\hypo! or \verb!\have!
+command produces an error message of the form:
+
+\begin{verbatim}
+ ! Package fitch Error: Undefined line reference: lab17.
+\end{verbatim}
+
+\subsection{Referencing line numbers in the text}
+\label{subsec-ndref}
+
+\DescribeMacro{\ndref}
+Labels defined in an \verb!nd! environment can be referenced in the
+text with the \verb!\ndref! command. This command takes a reference
+list as an argument, and produces the corresponding output. However,
+it is only possible to reference labels \emph{after} the corresponding
+derivation has been typeset. There is currently no convenient way of
+defining forward references. Also, if a label is used more than once,
+\verb!\ndref! will always refer to the most recent time it was used.
+
+\subsection{Scope}
+
+The commands \verb!\hypo!, \verb!\have!, \verb!\open!, \verb!\close!,
+\verb!\r!, \verb!\ii!, and so forth are only available inside an
+\verb!nd! environment. These commands may have a different meaning
+elsewhere in the same document. The only commands provided by the
+\verb!fitch.sty! package which are visible outside an \verb!nd!
+environment are the command \verb!\ndref! described in
+Section~\ref{subsec-ndref}, and the command \verb!\nddim! and the
+dimension \verb!\ndindent! described in Section~\ref{subsec-nddim}.
+
+\subsection{Breaking it across pages}\label{subsec-break}
+
+\DescribeMacro{\ndresume}
+The \verb!nd! environment is derived from the {\LaTeX} \verb!array!
+environment, and thus it does not break across pages automatically.
+However, if a derivation is too long to fit on a single page, it is
+possible to split it manually into physically independent, but
+logically consecutive subparts. For this purpose, the \verb!ndresume!
+environment is provided to continue a previously interrupted
+derivation. Here is an example:
+
+\begin{LTXexample}
+$
+\begin{nd}
+ \hypo {1} {P\vee Q}
+ \hypo {2} {\neg Q}
+ \open
+ \hypo {3} {P}
+ \have {4} {P} \r{3}
+ \close
+ \open
+ \hypo {aa} {Q}
+ \have {6} {\neg Q} \r{2}
+\end{nd}
+$
+
+Derivations can be interrupted and
+resumed at any point.
+
+$
+\begin{ndresume}
+ \have {7} {\bot} \ne{aa,6}
+ \have {8} {P} \be{7}
+ \close
+ \have {9} {P} \oe{1,3-4,aa-8}
+\end{ndresume}
+$
+\end{LTXexample}
+
+\subsection{Custom line numbers}
+
+One often needs to write derivation schemas, rather than derivations.
+This often requires the use of symbolic constants such as $n$, $n+1$,
+etc, instead of actual line numbers. The \verb!\have! and \verb!\hypo!
+commands have an optional first argument which is a symbolic constant.
+For instance, \verb!\have[n]! will cause the current line to be
+numbered with the symbolic constant $n$. Subsequent lines are
+automatically numbered $n+1$ etc. An initial offset can be given as a
+second optional argument, as in \verb!\have[n][-1]!, which will cause
+the current line to be numbered $n-1$, the following line $n$, etc. In
+an explicit offset is given, the symbolic constant can also be absent:
+for instance, the command \verb!\have[][7]! resets the current line
+number to $7$. The following example illustrates this behavior:
+
+\begin{LTXexample}
+\[
+\begin{nd}
+ \hypo {1} {P\vee Q}
+ \open
+ \hypo {2} {P}
+ \have [\vdots] {3} {\vdots}
+ \have [n][-1] {4} {A\wedge B}
+ \close
+ \open
+ \hypo {5} {Q}
+ \have [\vdots] {6} {\vdots}
+ \have [m] {7} {A\wedge B}
+ \close
+ \have {8} {A\wedge B} \oe{1,2-(4),5-7}
+ \have [\vdots] {9} {\vdots}
+ \have [][100] {10} {A} \ae{8}
+\end{nd}
+\]
+\end{LTXexample}
+
+Note that in the justification for line $m+1$, parentheses had to be
+put around the label $4$. There is currently no way of doing this
+automatically.
+
+{\bf Exercise.} How does one typeset an empty line number?
+
+{\bf Solution.} Since \verb!\have[]! has a special meaning as explained
+above, we need to use \verb!\have[~]! instead.
+
+\subsection{Continuation lines}\label{subsec-continuation}
+
+Sometimes one has to typeset a very long formula that does not fit on
+a single line. As of version 0.5 of the {\tt fitch.sty} macros, it is
+possible to break a formula into several lines using \verb!\\! as a
+line separator. Continuation lines are automatically indented, as
+shown in the following example.
+
+\begin{LTXexample}
+\[
+\begin{nd}
+ \hypo{1} {A\wedge B}
+ \hypo{2} {A\wedge B\rightarrow{} \\
+ C\wedge D}
+ \have{3} {C\wedge D} \ie{1,2}
+ \have{4} {A\wedge B\wedge{} \\
+ C\wedge D} \ai{1,3}
+\end{nd}
+\]
+\end{LTXexample}
+
+\DescribeMacro{\hypocont}
+\DescribeMacro{\havecont}
+Alternatively, the \verb!\havecont! and \verb!\hypocont! commands can
+be used to specify each continuation line separately, as the following
+example illustrates.
+
+\begin{LTXexample}
+\[
+\begin{nd}
+ \hypo{1} {A\wedge B}
+ \hypo{2} {A\wedge B\rightarrow{}}
+ \hypocont {C\wedge D}
+ \have{3} {C\wedge D} \ie{1,2}
+ \have{4} {A\wedge B\wedge{}} \ai{1,3}
+ \havecont {C\wedge D}
+\end{nd}
+\]
+\end{LTXexample}
+
+This latter style gives slightly more flexibility in the placement of
+justifications, since each line and continuation line can have its own
+justification and its own guard (via the \verb!\guard! command). It
+also allows a derivation to be interrupted between a line and its
+continuation, as discussed in Section~\ref{subsec-break}.
+
+\subsection{Customizing dimensions}\label{subsec-nddim}
+
+\DescribeMacro{\nddim}
+The relative sizes of the various elements of a natural deduction
+proof are preset to reasonable values depending on the size of the
+currently selected font. However, it will sometimes be necessary to
+customize these dimensions. This can be achieved with the
+\verb!\nddim! command. The syntax of the command is as follows:
+\begin{center}
+ \cmd{\nddim}\marg{height}\marg{topheight}\marg{depth}\marg{labelsep}
+ \marg{indent}\marg{hsep}\marg{justsep}\marg{linethickness},
+\end{center}
+where each of the eight parameters is a dimension. The meaning of the
+first seven parameters is shown in the
+following illustrations; \emph{linethickness} is simply the thickness
+of the lines.
+\[\includegraphics{fitchdoc-dimen}\]
+The default dimensions are:
+\begin{center}
+\verb!\nddim{4.5ex}{3.5ex}{1.5ex}{1em}{1.6em}{.5em}{2.5em}{.2mm}!.
+\end{center}
+\DescribeMacro{\ndindent}
+In addition, the dimension \verb!\ndindent!, controls
+the amount of extra indentation used on continuation lines as
+discussed in Section~\ref{subsec-continuation}. It can be changed and
+is \verb!1ex! by default.
+
+\subsection{Other comments}
+
+The goal was to design a flexible package which would not impose any
+constraints on the form of derivations, while making typesetting easy.
+With this package, it is in fact possible to typeset incomplete,
+ill-formed, or invalid derivations. Sometimes it is pedagogically necessary
+to do so.
+
+There are no arbitrary limits on the size or nesting depth of a derivation,
+except for the obvious requirement of fitting horizontally on the
+printed page.
+
+\section{Copyright and license}
+
+This document and the accompanying \verb!fitch.sty! macros
+are {\copyright} 2002--2023 by Peter Selinger and distributed under
+the terms of the \href{https://www.latex-project.org/lppl/}{LPPL}.
+
+\end{document}
Property changes on: trunk/Master/texmf-dist/doc/latex/fitch/fitchdoc.tex
___________________________________________________________________
Added: svn:eol-style
## -0,0 +1 ##
+native
\ No newline at end of property
Added: trunk/Master/texmf-dist/doc/latex/fitch/fitchexample.png
===================================================================
(Binary files differ)
Index: trunk/Master/texmf-dist/doc/latex/fitch/fitchexample.png
===================================================================
--- trunk/Master/texmf-dist/doc/latex/fitch/fitchexample.png 2023-09-04 23:43:36 UTC (rev 68178)
+++ trunk/Master/texmf-dist/doc/latex/fitch/fitchexample.png 2023-09-05 20:05:11 UTC (rev 68179)
Property changes on: trunk/Master/texmf-dist/doc/latex/fitch/fitchexample.png
___________________________________________________________________
Added: svn:mime-type
## -0,0 +1 ##
+application/octet-stream
\ No newline at end of property
Added: trunk/Master/texmf-dist/tex/latex/fitch/fitch.sty
===================================================================
--- trunk/Master/texmf-dist/tex/latex/fitch/fitch.sty (rev 0)
+++ trunk/Master/texmf-dist/tex/latex/fitch/fitch.sty 2023-09-05 20:05:11 UTC (rev 68179)
@@ -0,0 +1,231 @@
+%% fitch.sty
+%% Macros for Fitch-style natural deduction
+%% Copyright 2002-2023 Peter Selinger
+%
+% This work may be distributed and/or modified under the
+% conditions of the LaTeX Project Public License, either version 1.3
+% of this license or (at your option) any later version.
+% The latest version of this license is in
+% https://www.latex-project.org/lppl.txt
+% and version 1.3c or later is part of all distributions of LaTeX
+% version 2008 or later.
+%
+% This work has the LPPL maintenance status `maintained'.
+%
+% The Current Maintainer of this work is Richard Zach <rzach at ucalgary.ca>
+%
+% This work consists of the files fitch.sty and fitchdoc.tex.
+
+% Original Author: Peter Selinger, Dalhousie University
+% Created: Jan 14, 2002
+% Modified: Sep 4, 2023
+% Version: 0.6
+% Copyright: (C) 2002-2005 Peter Selinger
+% Filename: fitch.sty
+% Documentation: fitchdoc.tex
+% https://github.com/OpenLogicProject/fitch/
+
+% USAGE EXAMPLE:
+%
+% The following is a simple example illustrating the usage of this
+% package. For detailed instructions and additional functionality, see
+% the user guide, which can be found in the file fitchdoc.tex.
+%
+% \[
+% \begin{nd}
+% \hypo{1} {P\vee Q}
+% \hypo{2} {\neg Q}
+% \open
+% \hypo{3a} {P}
+% \have{3b} {P} \r{3a}
+% \close
+% \open
+% \hypo{4a} {Q}
+% \have{4b} {\neg Q} \r{2}
+% \have{4c} {\bot} \ne{4a,4b}
+% \have{4d} {P} \be{4c}
+% \close
+% \have{5} {P} \oe{1,3a-3b,4a-4d}
+% \end{nd}
+% \]
+
+\NeedsTeXFormat{LaTeX2e}
+\ProvidesPackage{fitch}[2023-09-04 v0.6 Macros for Fitch-style natural deduction]
+
+{\chardef\x=\catcode`\*
+\catcode`\*=11
+\global\let\nd*astcode\x}
+\catcode`\*=11
+
+% 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}
+
+% 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}
+
+\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}}
+
+% 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%
+ {\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*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}&}
+
+\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}
+
+% 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
+
+% 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}}
+
+% 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\ii{\by{$\Rightarrow$I}}%
+ \def\ie{\by{$\Rightarrow$E}}%
+ \def\Ai{\by{$\forall$I}}%
+ \def\Ae{\by{$\forall$E}}%
+ \def\Ei{\by{$\exists$I}}%
+ \def\Ee{\by{$\exists$E}}%
+ \def\ai{\by{$\wedge$I}}%
+ \def\ae{\by{$\wedge$E}}%
+ \def\ai{\by{$\wedge$I}}%
+ \def\ae{\by{$\wedge$E}}%
+ \def\oi{\by{$\vee$I}}%
+ \def\oe{\by{$\vee$E}}%
+ \def\ni{\by{$\neg$I}}%
+ \def\ne{\by{$\neg$E}}%
+ \def\be{\by{$\bot$E}}%
+ \def\nne{\by{$\neg\neg$E}}%
+ \def\r{\by{R}}%
+}
+
+\newenvironment{nd}{\begingroup\nd*init\nd*beginc}{\nd*endc\endgroup}
+\newenvironment{ndresume}{\begingroup\nd*init\nd*resumec}{\nd*endc\endgroup}
+
+\catcode`\*=\nd*astcode
+
+% End of file fitch.sty
+
Property changes on: trunk/Master/texmf-dist/tex/latex/fitch/fitch.sty
___________________________________________________________________
Added: svn:eol-style
## -0,0 +1 ##
+native
\ No newline at end of property
Modified: trunk/Master/tlpkg/bin/tlpkg-ctan-check
===================================================================
--- trunk/Master/tlpkg/bin/tlpkg-ctan-check 2023-09-04 23:43:36 UTC (rev 68178)
+++ trunk/Master/tlpkg/bin/tlpkg-ctan-check 2023-09-05 20:05:11 UTC (rev 68179)
@@ -337,7 +337,7 @@
fig4latex figbas figbib figchild figflow figput figsize
filecontents filecontentsdef filedate filehook fileinfo filemod
findhyph fink finstrut fira firamath firamath-otf
- first-latex-doc firstaid fistrum fitbox fithesis
+ first-latex-doc firstaid fistrum fitbox fitch fithesis
fix2col fixcmex fixdif fixfoot fixjfm fixlatvian
fixltxhyph fixmath fixme fixmetodonotes fixpdfmag fiziko
fjodor
Modified: trunk/Master/tlpkg/tlpsrc/collection-mathscience.tlpsrc
===================================================================
--- trunk/Master/tlpkg/tlpsrc/collection-mathscience.tlpsrc 2023-09-04 23:43:36 UTC (rev 68178)
+++ trunk/Master/tlpkg/tlpsrc/collection-mathscience.tlpsrc 2023-09-05 20:05:11 UTC (rev 68179)
@@ -94,6 +94,7 @@
depend extpfeil
depend faktor
depend fascicules
+depend fitch
depend fixdif
depend fixmath
depend fnspe
Added: trunk/Master/tlpkg/tlpsrc/fitch.tlpsrc
===================================================================
More information about the tex-live-commits
mailing list.