%%
%% 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'.
