-
Notifications
You must be signed in to change notification settings - Fork 0
/
main.tex
68 lines (47 loc) · 1.28 KB
/
main.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
\documentclass[11pt, oneside]{article} % use "amsart" instead of "article" for AMSLaTeX format
\usepackage{amsthm}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{syntax}
\usepackage{bm}
\usepackage{bussproofs}
\usepackage{hyperref}
\usepackage{thmtools}
\declaretheorem[style = definition, qed = $\square$]{definition}
\declaretheorem[style = remark, qed = $\square$]{notation}
\theoremstyle{plain}
\newtheorem{lemma}{Lemma}
\theoremstyle{plain}
\newtheorem{attempt} {Attempt}
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{innerex}{Exercise}
\newenvironment{ex}[1]
{\renewcommand\theinnerex{#1}\innerex}
{\endinnerex}
%Create a solution environment
%\newenvironment{solution}
% {\renewcommand\qedsymbol{$\blacksquare$}\begin{proof}[Solution]}
%{\end{proof}}
\newenvironment{solution}
{\begin{proof}[Solution]}
{\end{proof}}
\title{Selected Investigations on Type Theory}
\author{P. Rocha}
\date{\today}
\begin{document}
\maketitle
%\section{}
%\subsection{}
\include{LambdaCalculus}
\include{STLCSyntaxSemantics}
\include{STLCTyping}
\include{NatBool}
\include{STLCNormalization}
\include{STLC+References}
\include{STLC+ReferencesTyping}
\include{Polymorphism
}
\end{document}