aboutsummaryrefslogtreecommitdiffstats
path: root/latex-fitch
diff options
context:
space:
mode:
Diffstat (limited to 'latex-fitch')
-rw-r--r--latex-fitch/PKGBUILD18
-rw-r--r--latex-fitch/fitch112
-rw-r--r--latex-fitch/fitch.install11
-rwxr-xr-xlatex-fitch/watch21
4 files changed, 162 insertions, 0 deletions
diff --git a/latex-fitch/PKGBUILD b/latex-fitch/PKGBUILD
new file mode 100644
index 0000000..dfa2de3
--- /dev/null
+++ b/latex-fitch/PKGBUILD
@@ -0,0 +1,18 @@
+# Maintainer: Mattias Andrée <`base64 -d`(bWFhbmRyZWUK)@member.fsf.org>
+# Contributor: Lawrence Lee <valheru@facticius.net>
+pkgname=latex-fitch
+pkgver=1.6
+pkgrel=1
+pkgdesc="A LaTeX package for Fitch-style proofs"
+arch=('any')
+url="http://folk.uio.no/johanw/FitchSty.html"
+license=('GPL')
+depends=('tetex')
+install=fitch.install
+source=(http://folk.uio.no/johanw/fitch.sty)
+md5sums=('d62bdd0267c217d6017baef950b9205a')
+
+build() {
+ mkdir -p $startdir/pkg/usr/share/texmf-dist/tex/latex/fitch || return 1
+ cp $startdir/fitch.sty $startdir/pkg/usr/share/texmf-dist/tex/latex/fitch || return 1
+}
diff --git a/latex-fitch/fitch b/latex-fitch/fitch
new file mode 100644
index 0000000..963010e
--- /dev/null
+++ b/latex-fitch/fitch
@@ -0,0 +1,112 @@
+% $Id: fitch.sty,v 1.6 2003/06/28 16:53:00 johanw Exp $
+
+% Macros for Fitch-style formal proofs
+% Johan W. Klüwer, June 10, 2001
+
+
+\RequirePackage{mdwtab,latexsym,amsmath,amsfonts,ifthen}
+
+
+% Line height in proofs
+\newlength{\fitchlineht}
+\setlength{\fitchlineht}{1.5\baselineskip}
+% Horizontal indent between proof levels
+\newlength{\fitchindent}
+\setlength{\fitchindent}{1em}
+% Indent to comment
+\newlength{\fitchcomind}
+\setlength{\fitchcomind}{2em}
+% Line number width
+\newlength{\fitchnumwd}
+\setlength{\fitchnumwd}{1em}
+
+% Altered from mdwtab.sty: shorter vline, for start of subproof
+\makeatletter
+\newcommand\fvline[1][\arrayrulewidth]{\vrule\@height.5\fitchlineht\@width#1\relax}
+\makeatother
+% Ordinary vertical line
+\newcommand{\fa}{\vline\hspace*{\fitchindent}}
+% Vertical line, shorter: Use at start of (sub)proof
+\newcommand{\fb}{\fvline\hspace*{\fitchindent}}
+% Hypothesis
+\newcommand{\fh}{\fvline%
+ \makebox[0pt][l]{{%
+ \raisebox{-1.4ex}[0pt][0pt]{\rule{1.5em}{\arrayrulewidth}}}}%
+ \hspace*{\fitchindent}}
+% Hypothesis, with longer vert line: for >1 hypothesis
+\newcommand{\fj}{\vline%
+ \makebox[0pt][l]{{%
+ \raisebox{-1.4ex}[0pt][0pt]{\rule{1.5em}{\arrayrulewidth}}}}%
+ \hspace*{\fitchindent}}
+% Modal subproof: takes argument = operator
+\newcommand{\fitchmodal}[1]{%
+ \makebox[0pt][r]{${}^{#1}$\,}\fvline\hspace*{\fitchindent}}
+\newcommand{\fn}{\fitchmodal{\Box}}% Box subproof
+\newcommand{\fp}{\fitchmodal{\Diamond}}% Diamond subproof
+% Modal subproof with hypothesis in first line (as in Fitch)
+\newcommand{\fitchmodalh}[1]{%
+ \makebox[0pt][r]{${}^{#1}$\,}%
+ \fvline%
+ \makebox[0pt][l]{{%
+ \raisebox{-1.4ex}[0pt][0pt]{\rule{1.5em}{\arrayrulewidth}}}}%
+ \hspace*{\fitchindent}}
+% Rule: formula introduction marker. \fr with line, \fs without line
+\newcommand{\fr}{%
+ \makebox[0pt][r]{${\rhd}$\,\,}\vline\hspace*{\fitchindent}}
+\newcommand{\fs}{%
+ \makebox[0pt][r]{${\rhd}$\,\,}}
+% Box around argument, like new variable in ql
+\newcommand{\fw}[1]{\fbox{\footnotesize $#1$}}
+
+%
+\newcounter{fitchcounter}
+\setcounter{fitchcounter}{0}
+%To avoid starting from 1, \setboolean{resetfitchcounter}{false}
+\newboolean{resetfitchcounter}
+\setboolean{resetfitchcounter}{true}
+%To avoid increasing numbers, \setboolean{increasefitchcounter}{false}
+\newboolean{increasefitchcounter}
+\setboolean{increasefitchcounter}{true}
+%\formatfitchcounter can be altered if need be, though only once per proof
+\newcommand{\formatfitchcounter}[1]{\arabic{#1}}
+%Typeset the counter
+\newcommand{\fitchcounter}{%
+ \ifthenelse{\boolean{increasefitchcounter}}{\addtocounter{fitchcounter}{1}}{}
+ \formatfitchcounter{fitchcounter}}
+
+%A line with a special number -- a tag, e.g. \ftag{\vdots}{}
+\newcommand{\ftag}[2]{\multicolumn{1}%
+ {!{\makebox[\fitchnumwd][r]{#1}\hspace{\fitchindent}}Ml@{\hspace{\fitchcomind}}}%
+ {#2}}
+
+\newenvironment{fitchnum}%
+{\ifthenelse{\boolean{resetfitchcounter}}{\setcounter{fitchcounter}{0}}{}
+ \begin{tabular}{!{\makebox[\fitchnumwd][r]{\fitchcounter }\hspace{\fitchindent}}Ml@{\hspace{\fitchcomind}}l}}%
+{\end{tabular}}
+
+\newenvironment{fitchunum}%
+{\begin{tabular}{!{\makebox[\fitchnumwd][r]{}\hspace{\fitchindent}}Ml@{\hspace{\fitchcomind}}l}}%
+{\end{tabular}}
+
+\newenvironment{fitch}{\renewcommand{\arraystretch}{1.5}
+ \begin{fitchnum}}{\end{fitchnum}}
+\newenvironment{fitch*}{\renewcommand{\arraystretch}{1.5}
+ \begin{fitchunum}}{\end{fitchunum}}
+
+% The following is useful for giving a numbered formula, then the proof.
+\newenvironment{flem}[2]%
+{\begin{eqnarray}
+ &#1\label{#2}\\
+ &\begin{fitch}}%
+ {\end{fitch}\notag\end{eqnarray}}
+
+%To write comment field for two consecutive lines, with brace
+\newcommand{\ftwocom}[1]{%
+ \parbox[t]{3cm}{
+ \raisebox{-.6\baselineskip}[\baselineskip][0pt]{%
+ $\left.
+ \begin{aligned}
+ \,\\ \,
+ \end{aligned}
+ \right\}$\quad #1}
+ }}
diff --git a/latex-fitch/fitch.install b/latex-fitch/fitch.install
new file mode 100644
index 0000000..e1c1d5e
--- /dev/null
+++ b/latex-fitch/fitch.install
@@ -0,0 +1,11 @@
+post_upgrade() {
+ echo " updating the filename database..."
+ texconfig-sys rehash
+ echo " done."
+}
+
+post_remove() {
+ echo " updating the filename database..."
+ texconfig-sys rehash
+ echo " done."
+}
diff --git a/latex-fitch/watch b/latex-fitch/watch
new file mode 100755
index 0000000..8dca4f7
--- /dev/null
+++ b/latex-fitch/watch
@@ -0,0 +1,21 @@
+#!/bin/sh
+
+[ -f fitch.sty ] && rm fitch.sty
+
+wget 'http://folk.uio.no/johanw/fitch.sty' -O fitch.sty >/dev/null 2>/dev/null
+
+if [ $? = 0 ]; then
+ [ -f unfetchable ] && rm unfetchable
+ md5sum fitch.sty > new-sum
+ touch sum
+ if [ "$(cat sum)" = "$(cat new-sum)" ]; then
+ rm new-sum
+ else
+ mv new-sum sum
+ echo 'latex-fitch' '('"$(cat sum)"')'
+ fi
+elif [ ! -f unfetchable ]; then
+ touch unfetchable
+ echo 'latex-fitch (unfetchable)'
+fi
+