source: Papers/cpp-policy-2012/lst-grafite.tex @ 3346

Last change on this file since 3346 was 2077, checked in by boender, 7 years ago
  • committed actual file instead of link
File size: 4.3 KB
Line 
1\lstdefinelanguage{grafite} {
2mathescape=true,
3texcl=false,
4keywords={record, with, match, let, rec, corec, inductive, definition, axiom,
5        qed, intro, intros, symmetry, simplify, rewrite, apply, elim, assumption,
6        left, cut, cases, auto, right, coercion, split, lemma, theorem, skip, constructor, copy, from, letin,
7        by, done, we, conclude, assume, need, to, prove, unfold, return, and, check,
8        notation, interpretation, lapply, repeat, try, as, clear, in, change, whd, exists},
9morekeywords={[2]include},
10%emph={[1]Type, Prop, nat, real}, emphstyle={[1]\textit},
11literate=       
12        {->}{{$\to$}}3         
13        {:>}{{$\mathrm{:>}$}}1         
14        {>->}{{$\mapsto$}}2             
15        {<=}{{$\leq$}}2                 
16        {>=}{{$\geq$}}2         
17        {<>}{{$\neq$}}1
18        {\\/}{{$\vee$}}1               
19        {<->}{{$\leftrightarrow$}}2
20        {FORALL\ }{{$\forall\,$}}1             
21        {EXISTS\ }{{$\exists\,$}}1
22        {ALPHA}{{$\alpha$}}1
23        {LAMBDA}{{$\lambda\,$}}1
24        {\\lambda}{{$\lambda\,$}}1
25        {LANGLE}{{$\langle$}}1
26        {RANGLE}{{$\rangle$}}1
27        {EQUIV}{{$\equiv$}}1
28        {SIGMA}{{$\Sigma$}}1
29        {PSI}{{$\Psi$}}1
30        {DOTS}{{$\ldots$}}1
31        {NOT}{{$\neg$}}1
32        {\\in}{{$\in$}}1
33        {𝟙}{{$\mathbf{1}$}}1
34        {𝟘}{{$\mathbf{0}$}}1
35        {/\\}{$\land$}1
36        {×}{{$\times\,$}}2
37        {\\x}{{$\times\,$}}2
38        {}{{:=}}1
39        {δ}{{$\delta$}}1
40        {λ}{{$\lambda\,$}}1
41        {}{{$\nleq\,$}}1
42        {}{{$\lor\,$}}1
43        {}{{$\bigvee$}}1
44        {}{{$\approx\,$}}1
45        {}{{$\forall\,$}}1
46        {}{{$\exists\,$}}1
47        {}{{$\leadsto\,$}}1
48        {}{{$\rightarrow\,$}}1
49        {}{{$\leftrightarrow$}}1
50        {}{{$\land\,$}}1
51        {}{{$\bigwedge$}}1
52        {}{{$\leq\,$}}1
53        {¬}{{$\lnot\,$}}1
54        {}{{$\ll\,$}}1
55        {}{{$\gg\,$}}1
56        {}{{$\,\Rightarrow\,\,$}}2
57        {=>}{{$\,\Rightarrow\,\,$}}2
58        {_0}{{$\,\Rightarrow_0\,\,$}}2
59        {=>_0}{{$\,\Rightarrow_0\,\,$}}2
60        {_1}{{$\,\Rightarrow_1\,$}}1
61        {_1.}{{$\,\Rightarrow_1\,$}}1
62        {_\\r1}{{$\,\Rightarrow_1^{r}\,$}}1
63        {_\\r2}{{$\,\Rightarrow_2^{r}\,$}}1
64        {=>_1}{{$\,\Rightarrow_1\,$}}1
65        {_2}{{$\,\Rightarrow_2\,$}}1
66        {_\\o2}{{$\,\Rightarrow_2^o\,$}}1
67        {_\\c2}{{$\,\Rightarrow_2^c\,$}}1
68        {_\\c3}{{$\,\Rightarrow_3^c\,$}}1
69        {_\\obp2}{{$\,\Rightarrow_2^{obp}\,$}}1
70        {_\\bp1}{{$\,\Rightarrow_1^{bp}\,$}}1
71        {_\\bp2}{{$\,\Rightarrow_2^{bp}\,$}}1
72        {_\\obt2}{{$\,\Rightarrow_2^{obt}\,$}}1
73        {_2.}{{$\,\Rightarrow_2\,$}}1
74        {=>_2}{{$\,\Rightarrow_2\,$}}1
75        {=_1}{{$=$}}1
76        {=_2}{{$=$}}1
77        {}{{$\vdash$}}1
78        {}{{$\Vdash\,$}}2
79        {}{{$\between$}}2
80        {><}{{$>\!\!\!\!\!<\,$}}2
81        {}{{$^-$}}1
82        {⎻*}{{$^{-*}$}}1
83        {\\sup\ }{{$\!^-\,$}}1
84        {\\sup\ ⎻*}{{$\!^{-*}\,$}}1
85        {\\sup\ *}{{$\!^{*}\,$}}1
86        {^*}{{$\!^{*}\,$}}1
87        {F*}{{F$^*$}}1
88        {G*}{{G$^*$}}1
89        {}{{$\circ\;$}}2
90        {Ω}{{$\Omega$}}1
91        {Ω^carrbt}{{$\Omega^{\mbox{carrbt}}$}}1
92        {Ω^A}{{$\Omega^A$}}1
93        {Ω^C}{{$\Omega^C$}}1
94        {Ω^U}{{$\Omega^U$}}1
95        {Ω^V}{{$\Omega^V$}}1
96        {Ω^X}{{$\Omega^X$}}1
97        {Ω^s}{{$\Omega^s$}}1
98        {}{{$\ddagger$}}1
99        {}{{$\dagger$}}1
100        {}{{$\subseteq\,$}}2
101        {}{{$\natural$}}1
102        {}{{$\cap$}}2
103        {}{{$\cup$}}2
104        {}{{$\bigcap$}}2
105        {}{{$\bigcup$}}2
106        {}{{$\in\,$}}2
107        {⎽o}{{$_o$}}1
108        {⎽f}{{$_f$}}1
109        {'\ \\sub\\c}{{'$\!_c$}}1
110        {\ \\sub\\c}{{$_c$}}1
111        {'\\sub\\c}{{'$\!_c$}}1
112        {\\sub\\c}{{$_c$}}1
113        {'\ \\sub\\f}{{'$\!_f$}}1
114        {\ \\sub\\f}{{$_f$}}1
115        {'\\sub\\f}{{'$\!_f$}}1
116        {\\sub\\f}{{$_f$}}1
117        {\\sup\ (form\ o)}{{$^{o_f}$}}1
118        {\\sup\ (concr\ o)}{{$^{o_c}$}}1
119        {(form\ o)}{{o$_f~$}}2
120        {(concr\ o)}{{o$_c~$}}2
121        {form\ o}{{o$_f~$}}2
122        {concr\ o}{{o$_c~$}}2
123        {Ω^(form\ o)}{{$\Omega^{o_f}~$}}2
124        {Ω^(concr\ o)}{{$\Omega^{o_c}~$}}2
125        {◊⎽t}{{$\Diamond_t$}}1
126        {□⎽t}{{$\boxempty_t$}}1
127        {⎽⇒}{{$_\Rightarrow$}}1
128        {o_operator_of_operator}{{o\_op\_of\_op}}2
129        {o_saturation_expansive}{{o\_sat\_expa}}2
130        {o_saturation_monotone}{{o\_sat\_monot}}2
131        {o_saturation_idempotent}{{o\_sat\_idemp}}2
132        {o_continuous_relation_of_continuous_relation}{{ocrel\_of\_crel}}2
133        {o_basic_topology_of_basic_topology}{{obtop\_of\_btop}}2
134        {basic_topology_of_basic_pair}{{btop\_of\_bp}}2
135        {o_basic_topology_of_o_basic_pair}{{o\_bt\_of\_o\_bp}}2
136        {^-1}{{$^{-1}$}}1
137        {^\ -1}{{$^{-1}$}}1
138        {\ \\sup\ -1}{{$^{-1}$}}1
139        {\\sup\ -1}{{$^{-1}$}}1
140        {\ \\sup-1}{{$^{-1}$}}1
141        {\\sup-1}{{$^{-1}$}}1
142        {...}{{$\ldots$}}1
143        ,
144tabsize=1,
145comment=[s]{(*}{*)},
146showstringspaces=true,
147emptylines=0,
148extendedchars=true,
149sensitive=false,
150captionpos=b,
151mathescape=true,
152keywordstyle=\bfseries,
153keywordstyle=[2]\bfseries,
154keywordstyle=[3]\bfseries,
155%backgroundcolor=\color{gray},
156frame=tblr,
157%frameround=tttt,
158columns=flexible,
159basicstyle=\footnotesize\tt,
160}
161
Note: See TracBrowser for help on using the repository browser.