Skip to content
Permalink
Branch: master
Find file Copy path
Find file Copy path
Fetching contributors…
Cannot retrieve contributors at this time
98 lines (66 sloc) 1.85 KB
\documentclass{article}
\usepackage[a4paper]{geometry}
\usepackage[toc,page]{appendix}
\usepackage{mathtools}
\usepackage{bussproofs}
\usepackage{minted}
\usepackage{agda}
\usepackage{agdafonts}
\usepackage{cite}
\newcommand{\citep}[1]{\cite{#1}}
\newcommand{\citet}[1]{\cite{#1}}
\usepackage{hyperref}
\newcommand{\inline}[1]{\mintinline{agda}{#1}}
\usepackage{amsthm}
\theoremstyle{definition}
\newtheorem{definition}[subsubsection]{Definition}
\newtheorem{example}[subsubsection]{Example}
\theoremstyle{plain}
\newtheorem{corollary}[subsubsection]{Corollary}
\newtheorem{lemma}[subsubsection]{Lemma}
\newtheorem{proposition}[subsubsection]{Proposition}
\newtheorem{theorem}[subsubsection]{Theorem}
\newcommand{\codeqed}{\vspace{-1.5\baselineskip}}
\begin{document}
\title{Tome: Natural Deduction in Agda}
\author{
Louis Warren \\
School of Mathematics and Statistics, University of Canterbury, New Zealand
}
\date{}
\maketitle
\tableofcontents
\section{Introduction}
\input{introduction.tex}
\section{Decidable.lagda}
\input{_minted.Decidable.gen}
\section{Nat.lagda}
\input{_minted.Nat.gen}
\section{List.lagda}
\input{_minted.List.gen}
\section{Vec.lagda}
\input{_minted.Vec.gen}
\section{Formula.lagda}
\input{_minted.Formula.gen}
\section{Ensemble.lagda}
\input{_minted.Ensemble.gen}
\section{Deduction.lagda}
\input{_minted.Deduction.gen}
\section{Formula equivalence}
\input{_minted.equivalence.gen}
\section{Scheme.lagda}
\input{_minted.Scheme.gen}
\section{Example: the drinker paradox}
\input{_minted.drinkerexample.gen}
\bibliography{bib}{}
\bibliographystyle{abbrv}
\begin{appendices}
\section{Context as a list}
\subsection{Computational definition}
\input{_minted.no-ensemble.gen}
\subsection{Expanded context definition}
\input{_minted.no-ensemble-quasi.gen}
\section{Texify.lagda}
\input{_minted.Texify.gen}
\end{appendices}
\end{document}
You can’t perform that action at this time.