-
Notifications
You must be signed in to change notification settings - Fork 0
/
notes-template.tex
79 lines (64 loc) · 1.49 KB
/
notes-template.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
69
70
71
72
73
74
75
76
77
78
79
\documentclass{notes}
\coursename{Logical Relations Mini-Course}
\lecnumber{1}
\title{Notes Template}
\author{Scribe Name}
\begin{document}
\maketitle
\begin{syntax}
\category[Expressions]{e}
% Each alternative is introduced on its own line.
\alternative{x}
\alternative{n}
\alternative{\lambda x . e}
\alternative{e_1 e_2}
\category[Values]{v}
\alternative{\lambda x . e}
% You can add vertical spacing between categories to visually group them.
\separate
% You can pass the amount of space explicitly if you want to manually control it:
% \separate[5ex]
\category[Types]{\tau}
\alternative{\mathbf{Nat}}
% You can place alternatives on a new line.
\\
\alternative{\tau_1 \rightarrow \tau_2}
\category[Contexts]{\Gamma}
\alternative{x_1 : \tau_1, \ldots, x_n : \tau_n}
% You can use words to describe more complicated properties of
% definitions if you don't want to use BNF.
\note{no repeats}
\note{unordered}
% Alternative layout if you want more space.
\category[Expressions]{e}
\groupleft{
\alternative{x}
\alternative{n}
}
\groupleft{
\alternative{\lambda x . e}
\alternative{e_1 e_2}
}
\end{syntax}
\begin{thm}[Optional Theorem Name]
Theorem Statement
\end{thm}
\begin{proof}
Proof here.
\end{proof}
\begin{lem}
Lemma Statement
\end{lem}
\begin{cor}
Corollary Statement
\end{cor}
\begin{prop}
Proposition Statement
\end{prop}
\begin{defn}[Word]
Definition of word.
\end{defn}
\begin{nb}
Note
\end{nb}
\end{document}