← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to notes/papers/iird/poly.fmt

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
notes/papers/iird/poly.fmt
1
 
%subst verb a           = "\text{\tt " a "}"
2
 
%subst verbatim a       = "\begin{tabbing}\tt'n" a "'n\end{tabbing}'n"
3
 
%subst verbnl           = "\\'n\tt "
4
 
%if style == tt
5
 
%subst inline a  = "\text{\texfamily " a "}"
6
 
%subst thinspace = "\Sp "
7
 
%subst code a    = "\begin{tabbing}\texfamily'n" a "'n\end{tabbing}'n"
8
 
%subst comment a = "{\rmfamily-{}- " a "}"
9
 
%subst nested a  = "{\rmfamily\enskip\{- " a " -\}\enskip}"
10
 
%subst pragma a  = "{\rmfamily\enskip\{-\#" a " \#-\}\enskip}"
11
 
%subst spaces a  = a
12
 
%subst special a = a
13
 
%subst space     = "~"
14
 
%subst newline   = "\\'n\texfamily "
15
 
%subst conid a   = "{\itshape " a "}"
16
 
%subst varid a   = a
17
 
%subst consym a  = a
18
 
%subst varsym a  = a
19
 
%subst numeral a = a
20
 
%subst char a    = "''" a "''"
21
 
%subst string a  = "\char34 " a "\char34 "
22
 
%if underlineKeywords
23
 
%subst keyword a = "\uline{" a "}"
24
 
%else
25
 
%subst keyword a = "{\bfseries " a "}"
26
 
%endif
27
 
%format \         = "\char''10"
28
 
%format .         = "\char''00"
29
 
%if not spacePreserving
30
 
%format alpha     = "\char''02"
31
 
%format beta      = "\char''03"
32
 
%format gamma     = "\char''11"
33
 
%format delta     = "\char''12"
34
 
%format pi        = "\char''07"
35
 
%format infty     = "\char''16"
36
 
%format intersect = "\char''22"
37
 
%format union     = "\char''23"
38
 
%format forall    = "\char''24"
39
 
%format exists    = "\char''25"
40
 
%format not       = "\char''05"
41
 
%format &&        = "\char''04"
42
 
%format ||        = "\char''37"
43
 
%format <-        = "\char''06"
44
 
%format ->        = "\char''31"
45
 
%format ==        = "\char''36"
46
 
%format /=        = "\char''32"
47
 
%format <=        = "\char''34"
48
 
%format >=        = "\char''35"
49
 
%endif
50
 
%if meta
51
 
%format M.a = "\ensuremath{a}"
52
 
%format M.b = "\ensuremath{b}"
53
 
%format M.c = "\ensuremath{c}"
54
 
%format M.d = "\ensuremath{d}"
55
 
%format M.e = "\ensuremath{e}"
56
 
%format M.f = "\ensuremath{f}"
57
 
%format M.g = "\ensuremath{g}"
58
 
%format M.h = "\ensuremath{h}"
59
 
%format M.i = "\ensuremath{i}"
60
 
%format M.j = "\ensuremath{j}"
61
 
%format M.k = "\ensuremath{k}"
62
 
%format M.l = "\ensuremath{l}"
63
 
%format M.m = "\ensuremath{m}"
64
 
%format M.n = "\ensuremath{n}"
65
 
%format M.o = "\ensuremath{o}"
66
 
%format M.p = "\ensuremath{p}"
67
 
%format M.q = "\ensuremath{q}"
68
 
%format M.r = "\ensuremath{r}"
69
 
%format M.s = "\ensuremath{s}"
70
 
%format M.t = "\ensuremath{t}"
71
 
%format M.u = "\ensuremath{u}"
72
 
%format M.v = "\ensuremath{v}"
73
 
%format M.w = "\ensuremath{w}"
74
 
%format M.x = "\ensuremath{x}"
75
 
%format M.y = "\ensuremath{y}"
76
 
%format M.z = "\ensuremath{z}"
77
 
%format M.A = "\ensuremath{A}"
78
 
%format M.B = "\ensuremath{B}"
79
 
%format M.C = "\ensuremath{C}"
80
 
%format M.D = "\ensuremath{D}"
81
 
%format M.E = "\ensuremath{E}"
82
 
%format M.F = "\ensuremath{F}"
83
 
%format M.G = "\ensuremath{G}"
84
 
%format M.H = "\ensuremath{H}"
85
 
%format M.I = "\ensuremath{I}"
86
 
%format M.J = "\ensuremath{J}"
87
 
%format M.K = "\ensuremath{K}"
88
 
%format M.L = "\ensuremath{L}"
89
 
%format M.M = "\ensuremath{M}"
90
 
%format M.N = "\ensuremath{N}"
91
 
%format M.O = "\ensuremath{O}"
92
 
%format M.P = "\ensuremath{P}"
93
 
%format M.Q = "\ensuremath{Q}"
94
 
%format M.R = "\ensuremath{R}"
95
 
%format M.S = "\ensuremath{S}"
96
 
%format M.T = "\ensuremath{T}"
97
 
%format M.U = "\ensuremath{U}"
98
 
%format M.V = "\ensuremath{V}"
99
 
%format M.W = "\ensuremath{W}"
100
 
%format M.X = "\ensuremath{X}"
101
 
%format M.Y = "\ensuremath{Y}"
102
 
%format M.Z = "\ensuremath{Z}"
103
 
%format M.alpha   = "\ensuremath{\alpha}"
104
 
%format M.beta    = "\ensuremath{\beta}"
105
 
%format M.gamma   = "\ensuremath{\gamma}"
106
 
%format M.delta   = "\ensuremath{\delta}"
107
 
%format M.epsilon = "\ensuremath{\epsilon}"
108
 
%format M.zeta    = "\ensuremath{\zeta}"
109
 
%format M.eta     = "\ensuremath{\eta}"
110
 
%format M.theta   = "\ensuremath{\theta}"
111
 
%format M.iota    = "\ensuremath{\iota}"
112
 
%format M.kappa   = "\ensuremath{\kappa}"
113
 
%format M.lambda  = "\ensuremath{\lambda}"
114
 
%format M.mu      = "\ensuremath{\mu}"
115
 
%format M.nu      = "\ensuremath{\nu}"
116
 
%format M.xi      = "\ensuremath{\xi}"
117
 
%format M.pi      = "\ensuremath{\pi}"
118
 
%format M.rho     = "\ensuremath{\rho}"
119
 
%format M.sigma   = "\ensuremath{\sigma}"
120
 
%format M.tau     = "\ensuremath{\tau}"
121
 
%format M.upsilon = "\ensuremath{\upsilon}"
122
 
%format M.phi     = "\ensuremath{\phi}"
123
 
%format M.chi     = "\ensuremath{\chi}"
124
 
%format M.psi     = "\ensuremath{\psi}"
125
 
%format M.omega   = "\ensuremath{\omega}"
126
 
%format M.Gamma   = "\ensuremath{\Gamma}"
127
 
%format M.Delta   = "\ensuremath{\Delta}"
128
 
%format M.Theta   = "\ensuremath{\Theta}"
129
 
%format M.Lambda  = "\ensuremath{\Lambda}"
130
 
%format M.Xi      = "\ensuremath{\Xi}"
131
 
%format M.Pi      = "\ensuremath{\Pi}"
132
 
%format M.Sigma   = "\ensuremath{\Sigma}"
133
 
%format M.Upsilon = "\ensuremath{\Upsilon}"
134
 
%format M.Phi     = "\ensuremath{\Phi}"
135
 
%format M.Psi     = "\ensuremath{\Psi}"
136
 
%format M.Omega   = "\ensuremath{\Omega}"
137
 
%format M.forall  = "\ensuremath{\forall}"
138
 
%format M.exists  = "\ensuremath{\exists}"
139
 
%format M.not     = "\ensuremath{\neg}"
140
 
%format ==>       = "\ensuremath{\Longrightarrow}"
141
 
%format <==       = "\ensuremath{\Longleftarrow}"
142
 
%format /\        = "\ensuremath{\wedge}"
143
 
%format \/        = "\ensuremath{\vee}"
144
 
%format M.=       = "\ensuremath{=}"
145
 
%format M./=      = "\ensuremath{\neq}"
146
 
%format M.<       = "\ensuremath{<}"
147
 
%format M.<=      = "\ensuremath{\leq}"
148
 
%format M.>=      = "\ensuremath{\geq}"
149
 
%format M.>       = "\ensuremath{>}"
150
 
%endif
151
 
%elif style == newcode
152
 
%subst comment a        = "-- " a
153
 
%subst nested a         = "{- " a " -}"
154
 
%subst code a           = a "'n"
155
 
%subst newline          = "'n"
156
 
%subst dummy            =
157
 
%subst pragma a         = "{-# " a " #-}"
158
 
%subst numeral a        = a
159
 
%subst keyword a        = a
160
 
%subst spaces a         = a
161
 
%subst special a        = a
162
 
%subst space            = " "
163
 
%subst conid a          = a
164
 
%subst varid a          = a
165
 
%subst consym a         = a
166
 
%subst varsym a         = a
167
 
%subst char a           = "''" a "''"
168
 
%subst string a         = "'d" a "'d"
169
 
%format #               = "#"
170
 
%format $               = "$"
171
 
%format %               = "%"
172
 
%format &               = "&"
173
 
%format \               = "\"
174
 
%elif style == math
175
 
%subst phantom a        = "\phantom{" a "\mbox{}}"
176
 
%subst comment a        = "\mbox{\qquad-{}- " a "}"
177
 
%subst nested a         = "\mbox{\enskip\{- " a " -\}\enskip}"
178
 
%if array
179
 
%subst code a           = "\[\begin{array}{@{}lcl}'n\hspace{\lwidth}&\hspace{\cwidth}&\\[-10pt]'n" a "'n\end{array}\]"
180
 
%subst column3 l c r    = "{}" l " & " c " & {" r "}"
181
 
%subst column1 a        = "\multicolumn{3}{@{}l}{" a "}"
182
 
%else
183
 
%subst code a           = "\begin{tabbing}'n\qquad\=\hspace{\lwidth}\=\hspace{\cwidth}\=\+\kill'n" a "'n\end{tabbing}"
184
 
%subst column3 l c r    = "$" l "$ \> \makebox[\cwidth]{$" c "$} \> ${" r "}$"
185
 
%subst column1 a        = "${" a "}$"
186
 
%endif
187
 
%subst newline          = "\\'n"
188
 
%subst blankline        = "\\[1mm]'n"
189
 
%let anyMath            = True
190
 
%elif style == poly
191
 
%subst comment a        = "\mbox{\onelinecomment " a "}"
192
 
%subst nested a         = "\mbox{\commentbegin " a " \commentend}"
193
 
%if array
194
 
%subst code a           = "\['n\begin{parray}\SaveRestoreHook'n" a "\ColumnHook'n\end{parray}'n\]\resethooks'n"
195
 
%else
196
 
%subst code a           = "\begingroup\par\noindent\advance\leftskip\mathindent\('n\begin{pboxed}\SaveRestoreHook'n" a "\ColumnHook'n\end{pboxed}'n\)\par\noindent\endgroup\resethooks'n"
197
 
%endif
198
 
%subst column c a       = "\column{" c "}{" a "}'n"
199
 
%subst fromto b e t     = "\fromto{" b "}{" e "}{{}" t "{}}'n"
200
 
%subst left             = "@{}l@{}"
201
 
%subst centered         = "@{}c@{}"
202
 
%subst dummycol         = "@{}l@{}"
203
 
%subst newline          = "\nextline'n"
204
 
%subst blankline        = "\nextline[\blanklineskip]'n"
205
 
%subst indent n         = "\hsindent{" n "}"
206
 
%let anyMath            = True
207
 
%endif
208
 
%if anyMath
209
 
%let autoSpacing        = True
210
 
%subst dummy            = "\cdot "
211
 
%subst inline a         = "\ensuremath{" a "}"
212
 
%subst hskip a          = "\hskip" a "em\relax"
213
 
%subst pragma a         = "\mbox{\enskip\{-\#" a " \#-\}\enskip}"
214
 
%if latex209
215
 
%subst numeral a        = "{\mathrm " a "}"
216
 
%subst keyword a        = "{\mathbf " a "}"
217
 
%else
218
 
%subst numeral a        = "\mathrm{" a "}"
219
 
%subst keyword a        = "\mathbf{" a "}"
220
 
%endif
221
 
%subst spaces a         = a
222
 
%subst special a        = a
223
 
%subst space            = "\;"
224
 
%subst conid a          = "\Conid{" a "}"
225
 
%subst varid a          = "\Varid{" a "}"
226
 
%subst consym a         = "\mathbin{" a "}"
227
 
%subst varsym a         = "\mathbin{" a "}"
228
 
%subst char a           = "\text{\tt ''" a "''}"
229
 
%subst string a         = "\text{\tt \char34 " a "\char34}"
230
 
%format _          = "\anonymous "
231
 
%format ->         = "\to "
232
 
%format <-         = "\leftarrow "
233
 
%format =>         = "\Rightarrow "
234
 
%format \          = "\lambda "
235
 
%format |          = "\mid "
236
 
%format {          = "\{\mskip1.5mu "
237
 
%format }          = "\mskip1.5mu\}"
238
 
%format [          = "[\mskip1.5mu "
239
 
%format ]          = "\mskip1.5mu]"
240
 
%format =          = "\mathrel{=}"
241
 
%format ..         = "\mathinner{\ldotp\ldotp}"
242
 
%format ~          =  "\mathord{\sim}"
243
 
%format @          =  "\mathord{@}"
244
 
%format .          = "\mathbin{\circ}"
245
 
%format !!         = "\mathbin{!!}"
246
 
%format ^          = "\mathbin{\uparrow}"
247
 
%format ^^         = "\mathbin{\uparrow\uparrow}"
248
 
%format **         = "\mathbin{**}"
249
 
%format /          = "\mathbin{/}"
250
 
%format `quot`     = "\mathbin{\Varid{`quot`}}"
251
 
%format `rem`      = "\mathbin{\Varid{`rem`}}"
252
 
%format `div`      = "\mathbin{\Varid{`div`}}"
253
 
%format `mod`      = "\mathbin{\Varid{`mod`}}"
254
 
%format :%         = "\mathbin{:\%}"
255
 
%format %          = "\mathbin{\%}"
256
 
%format :          = "\mathbin{:}"
257
 
%format ++         = "\plus "
258
 
%format ==         = "\equiv "
259
 
%% ODER: format ==         = "\mathrel{==}"
260
 
%format /=         = "\not\equiv "
261
 
%% ODER: format /=         = "\neq "
262
 
%format <=         = "\leq "
263
 
%format >=         = "\geq "
264
 
%format `elem`     = "\in "
265
 
%format `notElem`  = "\notin "
266
 
%format &&         = "\mathrel{\wedge}"
267
 
%format ||         = "\mathrel{\vee}"
268
 
%format >>         = "\sequ "
269
 
%format >>=        = "\bind "
270
 
%format $          = "\mathbin{\$}"
271
 
%format `seq`      = "\mathbin{\Varid{`seq`}}"
272
 
%format !          = "\mathbin{!}"
273
 
%format //         = "\mathbin{//}"
274
 
%format undefined  = "\bot "
275
 
%format not        = "\neg "
276
 
%if meta
277
 
%format M.a = "a"
278
 
%format M.b = "b"
279
 
%format M.c = "c"
280
 
%format M.d = "d"
281
 
%format M.e = "e"
282
 
%format M.f = "f"
283
 
%format M.g = "g"
284
 
%format M.h = "h"
285
 
%format M.i = "i"
286
 
%format M.j = "j"
287
 
%format M.k = "k"
288
 
%format M.l = "l"
289
 
%format M.m = "m"
290
 
%format M.n = "n"
291
 
%format M.o = "o"
292
 
%format M.p = "p"
293
 
%format M.q = "q"
294
 
%format M.r = "r"
295
 
%format M.s = "s"
296
 
%format M.t = "t"
297
 
%format M.u = "u"
298
 
%format M.v = "v"
299
 
%format M.w = "w"
300
 
%format M.x = "x"
301
 
%format M.y = "y"
302
 
%format M.z = "z"
303
 
%format M.A = "A"
304
 
%format M.B = "B"
305
 
%format M.C = "C"
306
 
%format M.D = "D"
307
 
%format M.E = "E"
308
 
%format M.F = "F"
309
 
%format M.G = "G"
310
 
%format M.H = "H"
311
 
%format M.I = "I"
312
 
%format M.J = "J"
313
 
%format M.K = "K"
314
 
%format M.L = "L"
315
 
%format M.M = "M"
316
 
%format M.N = "N"
317
 
%format M.O = "O"
318
 
%format M.P = "P"
319
 
%format M.Q = "Q"
320
 
%format M.R = "R"
321
 
%format M.S = "S"
322
 
%format M.T = "T"
323
 
%format M.U = "U"
324
 
%format M.V = "V"
325
 
%format M.W = "W"
326
 
%format M.X = "X"
327
 
%format M.Y = "Y"
328
 
%format M.Z = "Z"
329
 
%format M.alpha   = "\alpha "
330
 
%format M.beta    = "\beta "
331
 
%format M.gamma   = "\gamma "
332
 
%format M.delta   = "\delta "
333
 
%format M.epsilon = "\epsilon "
334
 
%format M.zeta    = "\zeta "
335
 
%format M.eta     = "\eta "
336
 
%format M.theta   = "\theta "
337
 
%format M.iota    = "\iota "
338
 
%format M.kappa   = "\kappa "
339
 
%format M.lambda  = "\lambda "
340
 
%format M.mu      = "\mu "
341
 
%format M.nu      = "\nu "
342
 
%format M.xi      = "\xi "
343
 
%format M.pi      = "\pi "
344
 
%format M.rho     = "\rho "
345
 
%format M.sigma   = "\sigma "
346
 
%format M.tau     = "\tau "
347
 
%format M.upsilon = "\upsilon "
348
 
%format M.phi     = "\phi "
349
 
%format M.chi     = "\chi "
350
 
%format M.psi     = "\psi "
351
 
%format M.omega   = "\omega "
352
 
%format M.Gamma   = "\Gamma "
353
 
%format M.Delta   = "\Delta "
354
 
%format M.Theta   = "\Theta "
355
 
%format M.Lambda  = "\Lambda "
356
 
%format M.Xi      = "\Xi "
357
 
%format M.Pi      = "\Pi "
358
 
%format M.Sigma   = "\Sigma "
359
 
%format M.Upsilon = "\Upsilon "
360
 
%format M.Phi     = "\Phi "
361
 
%format M.Psi     = "\Psi "
362
 
%format M.Omega   = "\Omega "
363
 
%format M.forall  = "\forall "
364
 
%format M.exists  = "\exists "
365
 
%format M.not     = "\neg "
366
 
%format ==>       = "\enskip\Longrightarrow\enskip "
367
 
%format <==       = "\enskip\Longleftarrow\enskip "
368
 
%format /\        = "\enskip\mathrel{\wedge}\enskip "
369
 
%format \/        = "\enskip\mathrel{\vee}\enskip "
370
 
%format M.=       = "="
371
 
%format M./=      = "\neq "
372
 
%format M.<       = "<"
373
 
%format M.<=      = "\leq "
374
 
%format M.>=      = "\geq "
375
 
%format M.>       = ">"
376
 
%endif
377
 
%endif
378
 
%if style /= newcode
379
 
%subst code a = "\begin{colorcode}'n" a "\end{colorcode}\resethooks'n" 
380
 
%endif