forked from florian-rabe/Teaching
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathmacros.sty
166 lines (134 loc) · 5.36 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
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
%%%%%%%%%%%%%%%%%%%%%%%%% formatting
\setlength{\parindent}{0pt}
\setlength{\parskip}{2pt}
\setcounter{topnumber}{2}
\setcounter{bottomnumber}{2}
\setcounter{totalnumber}{4} % 2 may work better
\newcommand{\defemph}[1]{{\bf #1}}
\newcommand{\highlightframe}[1]{\noindent\fbox{\parbox{.99\textwidth}{\centering#1}}}
% generate toc entry for the bibliography
\newcommand{\tocentryBib}{
\cleardoublepage
\phantomsection
\addcontentsline{toc}{part}{Bibliography}
}
%%%%%%%%%%%%%%%%%%%%%%%%% logic
\renewcommand{\|}{\,|\,} %% produces || otherwise
\newcommand{\FORM}{\mathtt{form}}
\newcommand{\TERM}{\mathtt{term}}
\newcommand{\VAR}{\mathtt{var}}
\newcommand{\false}{\op{false}}
\newcommand{\true}{\op{true}}
\let\Equiv=\equiv
\renewcommand{\equiv}{\darr}
\newcommand{\arit}{\op{ar}}
\newcommand{\isterm}[4][]{#3\der^{#1}_{#2}#4:\TERM}
\newcommand{\istermS}[2]{\isterm{\Sigma}{#1}{#2}}
\newcommand{\istermSG}[1]{\isterm{\Sigma}{\Gamma}{#1}}
\newcommand{\isform}[4][]{#3\der^{#1}_{#2}#4:\FORM}
\newcommand{\isformS}[2]{\isform{\Sigma}{#1}{#2}}
\newcommand{\isformSG}[1]{\isform{\Sigma}{\Gamma}{#1}}
\newcommand{\sub}[2]{#1/#2}
\newcommand{\gSigma}{{\color{gray}\Sigma}}
\newcommand{\gDelta}{{\color{gray}\Delta}}
\newcommand{\gGamma}{{\color{gray}\Gamma}}
\newcommand{\iscons}[5][]{#3\ifnonempty{#4}{\ifnonempty{#3}{;}#4}\der^{#1}_{#2}#5} %% \iscons[L]{\Sigma}{\Gamma}{\Theta}{F}
\newcommand{\isconsgSGD}[1]{\iscons{\gSigma}{\gGamma}{\gDelta}{#1}} %% \isconsSGD{F}
\newcommand{\PL}{{\mathcal{PL}}}
\newcommand{\FOL}{{\mathcal{FOL}}}
\newcommand{\SFOL}{{\mathcal{SFOL}}}
\newcommand{\FOLEQ}{{\mathcal{FOLEQ}}}
\newcommand{\STT}{{\mathcal{STT}}}
\newcommand{\HOL}{{\mathcal{HOL}}}
%\newcommand{\SIG}{\mathtt{Sig}}
%\newcommand{\CONT}{\mathtt{Ctx}}
\newcommand{\TYPE}{\mathtt{type}}
\newcommand{\issig}[2][]{\der^{#1} #2}
\newcommand{\ismorph}[4][]{\der^{#1} #4:#2\arr#3}
\newcommand{\iscont}[3][]{\der^{#1}_{#2}#3\;\checkmark}
\newcommand{\issubs}[5][]{\der^{#1}_{#2}#5:#3\arr #4}
\newcommand{\istype}[3][]{\der^{#1}_{#2}#3:\TYPE}
\newcommand{\oftype}[5][]{#3\der^{#1}_{#2}#4\;:\;#5}
\newcommand{\istrue}[3][]{\der^{#1}_{#2}#3}
\newcommand{\isdecl}[4][]{#3\der^{#1}_{#2}#4\;\checkmark}
\newcommand{\lam}[2]{\lambda #1:#2.}
\newcommand{\Boole}{\mathbb{B}}
\newcommand{\PROOF}{\mathtt{proof}}
\newcommand{\LF}{{\mathcal{LF}}}
\newcommand{\KIND}{\mathtt{kind}}
\newcommand{\isdsig}[1]{\der #1}
\newcommand{\isdcont}[2]{\der_{#1}#2}
\newcommand{\isdsubs}[4]{\der_{#1}#4:#2\arr #3}
\newcommand{\isdkind}[4][]{#3\der^{#1}_{#2}#4:\KIND}
\newcommand{\ofdkind}[5][]{#3\der^{#1}_{#2}#4\;:\;#5}
\newcommand{\ofdtype}[5][]{#3\der^{#1}_{#2}#4\;:\;#5}
\newcommand{\isdequal}[5][]{#3\der^{#1}_{#2}#4\;=\;#5}
\newcommand{\evcont}[4][]{\der^{#1}_{#2}#3\;\rewrites\;#4}
\newcommand{\evdec}[5][]{#3\der^{#1}_{#2}#4\;\rewrites\;#5}
\newcommand{\evobj}[5][]{#3\der^{#1}_{#2}#4\;\rewrites\;#5}
%\renewcommand{\P}[2]{\Pi #1:#2.}
\newcommand{\rlname}[1]{\ensuremath{\mathtt{#1}}}
\newcommand{\rnsep}{\;\#\;}
\renewcommand{\dotatend}{.} %% put dot at end of Twelf declarations
\newcommand{\Type}{\mathtt{tp}}
\newcommand{\Term}{\mathtt{tm}}
\newcommand{\Fun}{\mathtt{\longrightarrow}}
\newcommand{\App}[2]{#1@#2}
\newcommand{\Lam}{\mathtt{lam}}
\newcommand{\Forms}{\op{Form}}
\newcommand{\FV}{\op{FV}}
\newcommand{\BV}{\op{BV}}
\renewcommand{\Con}{\op{Con}}
\newcommand{\val}{\der}
\newcommand{\univ}{\TERM}
\newcommand{\sem}[1]{\llbracket #1\rrbracket}
\newcommand{\semm}[2]{\sem{#1}^{#2}}
\newcommand{\semcm}[3]{\sem{#1|#2}^{#3}}
\newcommand{\md}{\models}
\newcommand{\reduce}[2]{#2|_{#1}}
\newcommand{\Thm}{\op{Thm}}
\newcommand{\Thy}{\op{Thy}}
\newcommand{\ModC}{\op{ModC}}
\newcommand{\galois}[1]{{#1}^\ast}
\newcommand{\closure}[1]{{#1}^\bullet}
\newcommand{\sM}{{\cal M}}
\newcommand{\kernel}[1]{\mathrm{ker}\, #1}
\newcommand{\image}[1]{\mathrm{im}\, #1}
\newcommand{\incllog}[2]{{#1}^{#2\harr}}
\newcommand{\theolog}[1]{\Th(#1)}
\newcommand{\found}{\mathcal{F}}
\newcommand{\Clause}{\op{Clauses}}
%\renewcommand{\rul}[3]{\ianc{#2}{#1}{#3}} %% only legacy for old logic notes
\newcommand{\inlineremark}[1]{{\hbox{}\hfill #1}}
\newcommand{\advanced}[1]{{\color{gray}#1}}
%%%%%%%%%%%%%%%%%%%%%%%%% datatypes
\newcommand{\Int}{\mathit{int}}
\newcommand{\Char}{\mathit{char}}
\newcommand{\String}{\mathit{string}}
\newcommand{\Unit}{\mathit{unit}}
\newcommand{\Void}{\mathit{void}}
\newcommand{\Bool}{\mathit{bool}}
\newcommand{\Enum}{\mathit{enum}}
\newcommand{\Float}{\mathit{float}}
%%%%%%%%%%%%%%%%%%%%%%%%% complexity
\newcommand{\incircbin}{\mathpalette\@incircbin}
\newcommand{\@incircbin}[2]{\mathbin{\ooalign{\hidewidth$#1#2$\hidewidth\crcr$#1\bigcirc$}}}
\newcommand{\oequal}{\incircbin{=}}
\newcommand{\oleq}{\incircbin{<}}
\newcommand{\compl}{\mathrm{Steps}}
\newcommand{\Oeq}[2]{#1 \oequal #2}
\newcommand{\Oleq}[2]{#1 \oleq #2}
\newcommand{\Poly}{\mathit{Poly}}
\newcommand{\Exp}{\mathit{Exp}}
% misc. examples
\newcommand{\inj}{\mathit{inj}}
\newcommand{\proj}{\mathit{proj}}
\newcommand{\inv}{\mathit{inv}}
\newcommand{\suc}{\mathit{succ}}
\newcommand{\modulus}{\mathit{modulus}}
\renewcommand{\mod}{\mathrm{mod}}
\newcommand{\modop}{\mathop{\mod}}
\newcommand{\divop}{\mathop{\mathrm{div}}}
\newcommand{\lcm}{\mathrm{lcm}}
%%%%%%%%%%%%%%%%%%%%%%%%%%% type theory
\newcommand{\form}{\mathtt{form}}