main.tex

% This is based on the LLNCS.DEM the demonstration file of
% the LaTeX macro package from Springer-Verlag
% for Lecture Notes in Computer Science,
% version 2.4 for LaTeX2e as of 16. April 2010
%
% See http://www.springer.com/computer/lncs/lncs+authors?SGWID=0-40209-0-0-0
% for the full guidelines.
%
\documentclass[11pt]{article}

\usepackage[utf8]{inputenc}
\usepackage[english]{babel}
\usepackage[margin=1in]{geometry}
\usepackage{amsmath,amsthm,amssymb,graphicx,stmaryrd}
\usepackage{hyperref,thmtools,enumitem,xcolor}

\newcommand{\vph}{\varphi}
\newcommand{\vep}{\varepsilon}
\newcommand{\N}{\mathbb{N}}
\newcommand{\Z}{\mathbb{Z}}
\newcommand{\U}{\mathsf{U}}
\renewcommand{\P}{\mathbb{P}}
\newcommand{\ctx}{\;\mathsf{ctx}}
\newcommand{\scott}[1]{\llbracket #1\rrbracket}
\newcommand{\ttag}[1]{\llparenthesis #1\rrparenthesis}
\newcommand{\elet}[2]{\mathsf{let}\;#1\mathrel{\mathsf{in}}#2}
\newcommand{\rec}{\mathsf{rec}}
\newcommand{\ok}{\ \mathsf{ok}}
\newcommand{\type}{\ \mathsf{type}}
\newcommand{\spec}{\ \mathsf{spec}}
\newcommand{\ctor}{\ \mathsf{ctor}}
\newcommand{\LE}{\ \mathsf{LE}}
\newcommand{\LEctor}{\ \mathsf{LE\;ctor}}
\newcommand{\mk}{\mathsf{mk}}
\newcommand{\lift}{\mathsf{lift}}
\newcommand{\sound}{\mathsf{sound}}
\newcommand{\acc}{\mathsf{acc}}
\newcommand{\intro}{\mathsf{intro}}
\newcommand{\inv}{\mathsf{inv}}
\newcommand{\inl}{\mathsf{inl}\;}
\newcommand{\inr}{\mathsf{inr}\;}
\newcommand{\up}{\mathsf{up}\;}
\newcommand{\dn}{\mathsf{dn}\;}
\newcommand{\ulift}{\mathsf{ulift}}
\renewcommand{\sup}{\mathsf{sup}\;}
\newcommand{\W}{\mathsf{W}}
\newcommand{\nonempty}{\mathsf{nonempty}}
\newcommand{\refl}{\mathsf{refl}}
\newcommand{\lvl}{\operatorname{lvl}}
\newcommand{\sort}{\operatorname{sort}}
\newcommand{\rank}{\operatorname{rank}}
\newcommand{\obj}{\mathsf{obj}}

\DeclareMathOperator{\imax}{imax}
\let\lGamma\Gamma \renewcommand{\Gamma}{\mathrm{\lGamma}}
\let\lDelta\Delta \renewcommand{\Delta}{\mathrm{\lDelta}}
\let\lSigma\Sigma \renewcommand{\Sigma}{\mathrm{\lSigma}}

\makeatletter
\providecommand{\leftsquigarrow}{\mathrel{\mathpalette\reflect@squig\relax}}
\newcommand{\reflect@squig}[2]{\reflectbox{$\m@th#1\rightsquigarrow$}}
\makeatother

\hypersetup{
    colorlinks,
    linkcolor={red!50!black},
    citecolor={blue!50!black},
    urlcolor={blue!80!black}
}

\addto\extrasenglish{
  \let\subsectionautorefname\sectionautorefname
  \let\subsubsectionautorefname\sectionautorefname
  \def\theoremautorefname{theorem}}

\declaretheorem[
name=Theorem,
refname={theorem,theorems},
Refname={Theorem,Theorems},
numberwithin=section]{theorem}
\declaretheorem[
name=Lemma,
refname={lemma,lemmas},
Refname={Lemma,Lemmas},
sibling=theorem]{lemma}
\newtheorem{remark}{Remark}
\declaretheorem[
name=Corollary,
refname={corollary,corollaries},
Refname={Corollary,Corollaries},
sibling=theorem]{corollary}
\newtheorem{definition}{Definition}
\setlist[itemize]{parsep=0pt,topsep=2pt,before=\leavevmode}
\setlist[enumerate]{parsep=0pt,topsep=2pt,before=\leavevmode}

\newlist{thmlist}{enumerate}{1}
\setlist[thmlist]{label=(\arabic{thmlisti}),
  ref=\thelemma.(\arabic{thmlisti}),
  parsep=0pt,topsep=2pt,before=\leavevmode}

\setlength{\parindent}{1em}
\setlength{\parskip}{.3em}

\begin{document}

\title{The Type Theory of Lean}
\author{Mario Carneiro}

\maketitle        % Print title page.
\tableofcontents  % Print table of contents

\input{intro}
\input{axioms}
\input{typesys}
\input{unique}
\input{Wtypes}
\input{soundness}
\input{normalization}
\input{compilation}

\end{document}