/
macros.sty
145 lines (119 loc) · 3.64 KB
/
macros.sty
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
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
\ProvidesPackage{macros}
%%%%% Names {{{
\newcommand{\stlc}{$λ^{→}$}
\newcommand{\lsyn}{$λ_{syn}^{→}$}
\newcommand{\mlsyn}{$\textsc{ML}_{syn}$}
\newcommand{\myth}{$\textsc{Myth}$}
\newcommand{\systemfsyn}{$λ_{syn}^{∀}$}
%%%%% }}}
%%%%% General typesetting {{{
\def\eg{\emph{e.g.\@\xspace}}
\def\ie{\emph{i.e.\@\xspace}}
\def\etc{\emph{etc.\@\xspace}}
\def\etal{\emph{et\ al.\@\xspace}}
% NOTE: so \autoref does the right thing for Chapter/Section capitalization
\addto\extrasenglish{%
\renewcommand{\chapterautorefname}{Chapter}
\renewcommand{\sectionautorefname}{Section}
\renewcommand{\subsectionautorefname}{Section}
}
\newcommand{\rulename}[1]{\textsc{#1}}
%%%%% }}}
%%%%% Math typesetting {{{
\newenvironment{proofenv}{%
\vspace{1em}
\hrule width \textwidth height 2pt depth 0mm
\vspace{0.25em}
\hrule
}{%
\hrule
\vspace{0.25em}
\hrule width \textwidth height 2pt depth 0mm
\vspace{1em}
}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}{Lemma}[section]
\newtheorem{property}{Property}[section]
\newtheorem{invariant}{Invariant}[section]
\newtheorem{definition}{Definition}[section]
\newtheorem{claim}{Claim}[section]
\theoremstyle{definition}
\newtheorem{example}{Example}[section]
\def\chapterautorefname{Chapter}
\def\lemmaautorefname{Lemma}
\def\propertyautorefname{Property}
\def\invariantautorefname{Invariant}
\def\definitionautorefname{Definition}
\def\claimautorefname{Claim}
\def\exampleautorefname{Example}
\def\listingautorefname{Listing}
\newcommand{\comma}{,}
\newcommand{\meq}{=}
\newcommand{\bnfalt}{\;\mathrel{\mid}\;}
\newcommand{\bnfdef}{%
\mathrel{\!\colon\!\!\colon\!\mathord{=}}%
}
\newcommand{\concat}{\mathbin{+\!\!+}}
\newcommand{\semisep}{\mathrel{;}}
\newcommand{\syn}[1]{\overset{#1}{⇝}}
\newcommand{\synE}{\syn{E}}
\newcommand{\synI}{\syn{I}}
\newcommand{\appprod}{\underset{app}{⊗}}
\def\⇥#1{\foreach \index in {1, ..., #1} {\quad}}
\newcommand{\alot}[1]{\overline{#1}}
\newcommand{\many}[2]{\overline{#1}^{#2}}
\newcommand{\mpf}{ρ}
\newcommand{\mkwd}[1]{\mathsf{#1}}
\newcommand{\mfun}[1]{\mathbf{#1}}
\newcommand{\mUnit}{\mkwd{Unit}}
\newcommand{\mbool}{\mkwd{bool}}
\newcommand{\mBool}{\mkwd{bool}}
\newcommand{\mtrue}{\mkwd{true}}
\newcommand{\mfalse}{\mkwd{false}}
\newcommand{\mfst}[1]{\mkwd{fst}\,#1}
\newcommand{\msnd}[1]{\mkwd{snd}\,#1}
\newcommand{\minl}[2][]{%
\ifthenelse{\equal{#1}{}}
{\mkwd{inl}\,#2}
{\mkwd{inl}_{#1}\;#2}
}
\newcommand{\minr}[2][]{%
\ifthenelse{\equal{#1}{}}
{\mkwd{inr}\,#2}
{\mkwd{inr}_{#1}\;#2}
}
\newcommand{\munit}{\mkwd{Unit}}
\newcommand{\mmatch}{\mkwd{match}}
\newcommand{\mwith}{\mkwd{with}}
\newcommand{\mfix}{\mkwd{fix}}
\newcommand{\mrec}{\mkwd{rec}}
\newcommand{\marg}[1]{\mkwd{arg}\,#1}
\newcommand{\mdec}[1]{\mkwd{dec}\,#1}
\newcommand{\mNoMatch}{\mkwd{NoMatch}}
\newcommand{\mgen}{\mfun{gen}}
\newcommand{\mrefine}{\mfun{refine}}
\newcommand{\mrtree}{\mfun{rtree}}
\newcommand{\mguess}{\mfun{guess}}
\newcommand{\mfmatch}{\mfun{match}}
\newcommand{\mrmatch}{\mfun{rmatch}}
\newcommand{\mfold}[1]{\mkwd{fold}\,#1}
\newcommand{\munfold}[1]{\mkwd{unfold}\,#1}
\newcommand{\mdata}{\mkwd{data}}
\newcommand{\mtype}{\mkwd{type}}
\newcommand{\mof}{\mkwd{of}}
\newcommand{\mlet}{\mkwd{let}}
\newcommand{\mexp}{\mkwd{exp}}
\newcommand{\mnat}{\mkwd{nat}}
\newcommand{\mS}{\mkwd{S}}
\newcommand{\mO}{\mkwd{O}}
\newcommand{\mlist}{\mkwd{list}}
\newcommand{\mNil}{\mkwd{Nil}}
\newcommand{\mCons}{\mkwd{Cons}}
\newcommand{\mtree}{\mkwd{tree}}
\newcommand{\mdyn}{\mkwd{dyn}}
\newcommand{\mError}{\mkwd{Error}}
\newcommand{\mBase}{\mkwd{Base}}
\newcommand{\mDyn}{\mkwd{Dyn}}
\newcommand{\pbox}[2]{\lceil #1 \rceil^{#2}}
\newcommand{\mfbox}{\mfun{box}}
%%%%% }}}