1 \usepackage{blindtext}
\r
2 \usepackage{enumerate}
\r
3 \usepackage{hyperref, bookmark}
\r
4 \usepackage{amsmath, amsfonts, amssymb, amsthm}
\r
6 \usepackage{bussproofs}
\r
9 \newtheorem{theorem}{Theorem}
\r
10 \newtheorem{lemma}{Lemma}
\r
11 % \newtheorem{prop}[thm]{Proposition}
\r
12 \newtheorem{corollary}{Corollary}
\r
14 \theoremstyle{definition}
\r
15 \newtheorem{definition}{Definition}
\r
16 % \newtheorem{conj}{Conjecture}[section]
\r
17 \newtheorem{example}{Example}
\r
19 % \theoremstyle{remark}
\r
20 % \newtheorem*{rem}{Remark}
\r
21 % \newtheorem*{note}{Note}
\r
23 \newcommand{\defeq}{:=}
\r
24 \newcommand{\underscore}{\_\!\_}
\r
26 \newcommand{\TmIdentity}{\operatorname{I}}
\r
27 \newcommand{\TmTrue}{\operatorname{tt}}
\r
28 \newcommand{\TmFalse}{\operatorname{ff}}
\r
30 \newcommand{\SepP}[2]{\langle #1 \mid #2\rangle}
\r
31 \newcommand{\Subtm}{\preceq}%{\trianglelefteq}
\r
32 \newcommand{\Subtmapp}{\preceq^a}
\r
33 \newcommand{\EtaEq}{=_\eta}
\r
34 \newcommand{\EtaNeq}{\not\EtaEq}
\r
35 \newcommand{\true}{\operatorname{tt}}
\r
36 \newcommand{\false}{\operatorname{ff}}
\r
37 \newcommand{\todo}[1]{{\color{red}#1}}
\r
38 \newcommand{\ddef}{\mathrel{::=}}
\r
39 \newcommand{\semi}{\mathrel{;}}
\r
41 \newcommand{\ih}{\emph{i.h.}}
\r
42 \newcommand{\ie}{\emph{i.e.}}
\r
43 \newcommand{\eg}{\emph{e.g.}}
\r
44 % \newcommand{\EtaNeq}{\mathrel{\texttt{<>}}}
\r
46 \newcommand{\Commento}[1]{{\bf\color{red}#1}}
\r
48 \newcommand{\LambdaFire}{$\lambda_f$}
\r
49 \newcommand{\NewSystem}{$\lambda_{\color{red}???}$}
\r
51 % explicit substitution objectified
\r
52 \newcommand{\en}[2]{\texttt{[}#2\texttt{/}#1\texttt{]}}
\r
53 \newcommand{\comma}{\texttt{,}}
\r
54 \renewcommand{\semi}{\texttt{;}}
\r
55 \newcommand{\as}{{\ast}} % asterisk
\r
57 \newcommand{\Operator}[1]{\texttt{#1}}
\r
58 \newcommand{\Match}[2]{\Operator{match}^{#1}\,#2}
\r
59 \newcommand{\Branch}[2]{#1\mathrel{\texttt{=>}}#2}
\r
60 \newcommand{\SepPA}[3]{\langle#1 \mid #2 \mid #3\rangle}
\r
61 \newcommand{\Sep}{\mathrel{\texttt{|}}}
\r
62 \newcommand{\Num}{\mathrm{N}}
\r
63 \newcommand{\Numeral}[1]{\bar{#1}}
\r
65 \newcommand{\ToFire}[1]{#1{\downarrow}}
\r
68 % from strong_fireballs macros.tex
\r
69 \newcommand{\Lam}[1]{\lambda #1.\,}
\r
71 \newcommand{\hl}[1]{{\underline{#1}}}
\r
72 \newcommand{\Esub}[2]{\texttt{[}#2\texttt{/}#1\texttt{]}}
\r
73 \newcommand{\Comma}{\texttt{,}}
\r
74 \newcommand{\Semi}{\texttt{;}}
\r
75 \newcommand{\Subst}[2]{\{#2/#1\}}
\r
76 % \newcommand{\Comma}{}
\r
78 \newcommand{\tmtwo}{u}
\r
79 \newcommand{\tmthree}{s}
\r
80 \newcommand{\var}{x}
\r
81 \newcommand{\vartwo}{y}
\r
82 \newcommand{\varthree}{z}
\r
83 \newcommand{\varfour}{w}
\r
85 \newcommand{\Red}[2]{\xrightarrow{#2}_{#1}}
\r
86 \newcommand{\TODO}{\textcolor{red}{TODO}}
\r
88 \renewcommand{\Lam}[2]{\lambda#1.\, \{\!\!\{#2\}\!\!\}}