%% %% This is file `lplfitch.sty', %% generated with the docstrip utility. %% %% The original source files were: %% %% lplfitch.dtx (with options: `package') %% %% This is a generated file. %% %% Copyright (C) 2013 by John Etchemendy, Dave Barker-Plummer and Richard Zach %% %% This file may be distributed and/or modified under the conditions of %% the LaTeX Project Public License, either version 1.2 of this license %% or (at your option) any later version. The latest version of this %% license is in: %% %% http://www.latex-project.org/lppl.txt %% %% and version 1.2 or later is part of all distributions of LaTeX version %% 1999/12/01 or later. %% \NeedsTeXFormat{LaTeX2e}[1999/12/01] \ProvidesPackage{lplfitch} [2013/05/16 v0.9 LPL Fitch style] \NeedsTeXFormat{LaTeX2e} \ProvidesPackage{lplfitch}[2013/05/07 -- Fitch Proofs a la LPL] \newcommand*{\formula}[1]{\ensuremath{\sf{#1}}} \newcommand*\lif{\rightarrow} \newcommand*\liff{\leftrightarrow} \newcommand*\lfalse{\bot} \newcommand*\lall{\forall} \newcommand*\lis{\exists} \newcommand*{\quant}[3]{#1 #2\;#3} \newcommand*{\exi}[2]{\quant{\lis}{#1}{#2}} \newcommand*{\uni}[2]{\quant{\lall}{#1}{#2}} \newcommand*\intro[1]{\formula{#1\,}{\bf Intro:}} \newcommand*\elim[1]{\formula{#1\,}{\bf Elim:}} \newcommand*\landi[1]{\intro{\land} #1} \newcommand*\lande[1]{\elim{\land} #1} \newcommand*\lori[1]{\intro{\lor} #1} \newcommand*\lore[3]{\elim{\lor} #1, #2, #3} \newcommand*\lnoti[1]{\intro{\lnot} #1} \newcommand*\lnote[1]{\elim{\lnot} #1} \newcommand*\lfalsei[2]{\intro{\lfalse} #1, #2} \newcommand*\lfalsee[1]{\elim{\lfalse} #1} \newcommand*\lifi[1]{\intro{\lif} #1} \newcommand*\life[2]{\elim{\lif} #1, #2} \newcommand*\liffi[2]{\intro{\liff} #1, #2} \newcommand*\liffe[2]{\elim{\liff} #1, #2} \newcommand*\reit[1]{{\bf Reit:} #1} \newcommand*\eqi[0]{$=\,${\bf Intro}} \newcommand*\eqe[2]{\elim{=} #1, #2} \newcommand*\lalli[1]{\intro{\lall} #1} \newcommand*\lalle[1]{\elim{\lall} #1} \newcommand*\lexii[1]{\intro{\lis} #1} \newcommand*\lexie[2]{\elim{\lis} #1, #2} \newlength{\fitchargwidth} \setlength{\fitchargwidth}{3.5in} \newlength{\fitchprfwidth} \setlength{\fitchprfwidth}{3.0in} \newlength{\fitchctxwidth} \setlength{\fitchctxwidth}{1in} \newlength{\fitchsep} \setlength{\fitchsep}{10pt} \newcommand{\fitchctx}[1]{% \advance \fitchctxwidth by -\fitchsep% \advance \fitchctxwidth by .5pt% \begin{tabular}[t]{r@{}|p{\fitchctxwidth}@{}l} \phantom{\slider} \\[-1.75ex] #1 \\[-1.75ex] & & \end{tabular} \advance \fitchctxwidth by \fitchsep% \advance \fitchctxwidth by -.5pt% } \newcommand{\fitchprf}[2]{% \advance \fitchprfwidth by -\fitchsep% \advance \fitchprfwidth by .5pt% \hspace*{.35em}% \begin{tabular}[t]{|p{0pt}@{}p{\fitchprfwidth}@{\hspace*{\fitchsep}}l} \multicolumn{3}{@{}l@{}}{\ }\\[-2.35ex] #1 \\ \ \\[-2.5ex] \cline{1-1}\\[-2ex] #2 \\ \multicolumn{3}{@{}l@{}} \ \\[-2.35ex] \end{tabular} \advance \fitchprfwidth by \fitchsep% } \newcommand{\fitcharg}[2]{ \advance \fitchargwidth by -\fitchsep% \hspace*{.35em} \begin{tabular}[t]{|p{\fitchsep}@{}p{\fitchargwidth}@{}} \multicolumn{2}{@{}l@{}}{\ }\\[-2.35ex] #1 \\ \ \\[-2.5ex] \cline{1-1}\\[-2ex] #2 \\ \multicolumn{2}{@{}l@{}} \ \\[-2.35ex] \end{tabular} } \newcommand*{\slider}{\mbox{$\triangleright \;$}} \def\pline{\@ifnextchar[\@plinenum{\@plinenum[\@empty]}} \def\@plinenum[#1]#2{\@ifnextchar[{\@plinex{#1}{#2}}{% \@plinex{#1}{#2}[\@empty]}} \def\@plinex#1#2[#3]{ & #1\formula{\; #2} & #3} \newcommand*\fpline{\slider\pline} \newcommand*{\tline}[2][{}]{ & #1\hspace{.6em}{#2}} \newcommand*{\nline}[2][{}]{ & #1\formula{\;#2}} \newcommand*{\jline}[2][{}]{\nline#2 & #1} \newcommand*{\fline}[1]{\slider \jline#1} \newcommand*{\ellipsesline}[0]{\nline{\;\raise.65ex\hbox{\vdots}}} \newcommand{\subproof}[2]{&\fitchprf{#1}{#2}\\} \newcommand{\boxedsubproof}[4][{}]{ \subproof{\nline[#1]{\fbox{\formula{#2}}\;#3}}{#4} } \newcommand{\brokenform}[2]{ \advance\fitchprfwidth by-\fitchsep \begin{tabular}[c]{rp{\fitchprfwidth}} \multicolumn{1}{p{\fitchprfwidth}@{}}{\formula{#1}}\\ \formula{#2} \end{tabular} \advance\fitchprfwidth by\fitchsep } \endinput %% %% End of file `lplfitch.sty'.