clean up latex junk

digama0 · Mar 17, 2018 · 50a9fd3 · 50a9fd3
1 parent cc1c436
commit 50a9fd3
Show file tree

Hide file tree

Showing 15 changed files with 83 additions and 5,445 deletions.
diff --git a/Wtypes.tex b/Wtypes.tex
@@ -53,7 +53,7 @@ \section{Reduction of inductive types to $\W$-types}
 1\le\ell\quad \Gamma\vdash C:\alpha\to\U_\ell\\
 \Gamma\vdash e:\forall x:\alpha.\; (\forall y:\alpha.\;r\;y\;x\to\acc_r\;y)\to (\forall y:\alpha.\;r\;y\;x\to C\;y)\to C\;x
 \end{matrix}}{\Gamma\vdash \rec_\acc\;e:\forall x:\alpha.\;\acc_r\;x\to C\;x}$$
-All of these could have been defined as inductive types in the sense of section \ref{inductive}:
+All of these could have been defined as inductive types in the sense of section \ref{sec:inductive}:
 \begin{align*}
 \bot&:=\mu t:\P.\;0\\
 \Sigma x:\alpha.\;\beta&:=\mu t:\U_{\max(\ell,\ell',1)}.\;(\mathsf{pair}:\forall x:\alpha.\;\beta\to t)\\

diff --git a/aliascnt.sty b/aliascnt.sty
diff --git a/history.txt b/history.txt
diff --git a/intro.tex b/intro.tex
@@ -1,2 +1,2 @@
 \section{Introduction}
-UNFINISHED
+In this paper, we develop the foundational theory used in the Lean theorem prover.