source: Papers/jar-cerco-2017/lst-grafite.tex @ 3657

Last change on this file since 3657 was 3657, checked in by mulligan, 3 years ago

more cannibalisation

File size: 4.6 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},
10keywordstyle=\color{blue}\bfseries,
11%emph={[1]Type, Prop, nat, real}, emphstyle={[1]\textit},
12% literate=     
13%       {->}{{$\to$}}3         
14%       {:>}{{$\mathrm{:>}$}}1         
15%       {>->}{{$\mapsto$}}2             
16%       {<=}{{$\leq$}}2                 
17%       {>=}{{$\geq$}}2         
18%       {<>}{{$\neq$}}1
19%       {\\/}{{$\vee$}}1               
20%       {<->}{{$\leftrightarrow$}}2
21%       {FORALL\ }{{$\forall\,$}}1             
22%       {EXISTS\ }{{$\exists\,$}}1
23%       {ALPHA}{{$\alpha$}}1
24%       {LAMBDA}{{$\lambda\,$}}1
25%       {\\lambda}{{$\lambda\,$}}1
26%       {LANGLE}{{$\langle$}}1
27%       {RANGLE}{{$\rangle$}}1
28%       {EQUIV}{{$\equiv$}}1
29%       {SIGMA}{{$\Sigma$}}1
30%       {PSI}{{$\Psi$}}1
31%       {DOTS}{{$\ldots$}}1
32%       {NOT}{{$\neg$}}1
33%       {\\in}{{$\in$}}1
34%       {𝟙}{{$\mathbf{1}$}}1
35%       {𝟘}{{$\mathbf{0}$}}1
36%       {/\\}{$\land$}1
37%       {×}{{$\times\,$}}2
38%       {\\x}{{$\times\,$}}2
39%       {≝}{{:=}}1
40%       {δ}{{$\delta$}}1
41%       {λ}{{$\lambda\,$}}1
42%       {≰}{{$\nleq\,$}}1
43%       {∨}{{$\lor\,$}}1
44%       {⋁}{{$\bigvee$}}1
45%       {≈}{{$\approx\,$}}1
46%       {∀}{{$\forall\,$}}1
47%       {∃}{{$\exists\,$}}1
48%       {⇝}{{$\leadsto\,$}}1
49%       {→}{{$\rightarrow\,$}}1
50%       {↔}{{$\leftrightarrow$}}1
51%       {∧}{{$\land\,$}}1
52%       {⋀}{{$\bigwedge$}}1
53%       {≤}{{$\leq\,$}}1
54%       {¬}{{$\lnot\,$}}1
55%       {≪}{{$\ll\,$}}1
56%       {≫}{{$\gg\,$}}1
57%       {⇒}{{$\,\Rightarrow\,\,$}}2
58%       {=>}{{$\,\Rightarrow\,\,$}}2
59%       {⇒_0}{{$\,\Rightarrow_0\,\,$}}2
60%       {=>_0}{{$\,\Rightarrow_0\,\,$}}2
61%       {⇒_1}{{$\,\Rightarrow_1\,$}}1
62%       {⇒_1.}{{$\,\Rightarrow_1\,$}}1
63%       {⇒_\\r1}{{$\,\Rightarrow_1^{r}\,$}}1
64%       {⇒_\\r2}{{$\,\Rightarrow_2^{r}\,$}}1
65%       {=>_1}{{$\,\Rightarrow_1\,$}}1
66%       {⇒_2}{{$\,\Rightarrow_2\,$}}1
67%       {⇒_\\o2}{{$\,\Rightarrow_2^o\,$}}1
68%       {⇒_\\c2}{{$\,\Rightarrow_2^c\,$}}1
69%       {⇒_\\c3}{{$\,\Rightarrow_3^c\,$}}1
70%       {⇒_\\obp2}{{$\,\Rightarrow_2^{obp}\,$}}1
71%       {⇒_\\bp1}{{$\,\Rightarrow_1^{bp}\,$}}1
72%       {⇒_\\bp2}{{$\,\Rightarrow_2^{bp}\,$}}1
73%       {⇒_\\obt2}{{$\,\Rightarrow_2^{obt}\,$}}1
74%       {⇒_2.}{{$\,\Rightarrow_2\,$}}1
75%       {=>_2}{{$\,\Rightarrow_2\,$}}1
76%       {=_1}{{$=$}}1
77%       {=_2}{{$=$}}1
78%       {⊢}{{$\vdash$}}1
79%       {⊩}{{$\Vdash\,$}}2
80%       {≬}{{$\between$}}2
81%       {><}{{$>\!\!\!\!\!<\,$}}2
82%       {⎻}{{$^-$}}1
83%       {⎻*}{{$^{-*}$}}1
84%       {\\sup\ ⎻}{{$\!^-\,$}}1
85%       {\\sup\ ⎻*}{{$\!^{-*}\,$}}1
86%       {\\sup\ *}{{$\!^{*}\,$}}1
87%       {^*}{{$\!^{*}\,$}}1
88%       {F*}{{F$^*$}}1
89%       {G*}{{G$^*$}}1
90%       {∘}{{$\circ\;$}}2
91%       {Ω}{{$\Omega$}}1
92%       {Ω^carrbt}{{$\Omega^{\mbox{carrbt}}$}}1
93%       {Ω^A}{{$\Omega^A$}}1
94%       {Ω^C}{{$\Omega^C$}}1
95%       {Ω^U}{{$\Omega^U$}}1
96%       {Ω^V}{{$\Omega^V$}}1
97%       {Ω^X}{{$\Omega^X$}}1
98%       {Ω^s}{{$\Omega^s$}}1
99%       {‡}{{$\ddagger$}}1
100%       {†}{{$\dagger$}}1
101%       {⊆}{{$\subseteq\,$}}2
102%       {♮}{{$\natural$}}1
103%       {∩}{{$\cap$}}2
104%       {∪}{{$\cup$}}2
105%       {⋂}{{$\bigcap$}}2
106%       {⋃}{{$\bigcup$}}2
107%       {∈}{{$\in\,$}}2
108%       {⎽o}{{$_o$}}1
109%       {⎽f}{{$_f$}}1
110%       {'\ \\sub\\c}{{'$\!_c$}}1
111%       {\ \\sub\\c}{{$_c$}}1
112%       {'\\sub\\c}{{'$\!_c$}}1
113%       {\\sub\\c}{{$_c$}}1
114%       {'\ \\sub\\f}{{'$\!_f$}}1
115%       {\ \\sub\\f}{{$_f$}}1
116%       {'\\sub\\f}{{'$\!_f$}}1
117%       {\\sub\\f}{{$_f$}}1
118%       {\\sup\ (form\ o)}{{$^{o_f}$}}1
119%       {\\sup\ (concr\ o)}{{$^{o_c}$}}1
120%       {(form\ o)}{{o$_f~$}}2
121%       {(concr\ o)}{{o$_c~$}}2
122%       {form\ o}{{o$_f~$}}2
123%       {concr\ o}{{o$_c~$}}2
124%       {Ω^(form\ o)}{{$\Omega^{o_f}~$}}2
125%       {Ω^(concr\ o)}{{$\Omega^{o_c}~$}}2
126%       {◊⎽t}{{$\Diamond_t$}}1
127%       {□⎽t}{{$\boxempty_t$}}1
128%       {⎽⇒}{{$_\Rightarrow$}}1
129%       {o_operator_of_operator}{{o\_op\_of\_op}}2
130%       {o_saturation_expansive}{{o\_sat\_expa}}2
131%       {o_saturation_monotone}{{o\_sat\_monot}}2
132%       {o_saturation_idempotent}{{o\_sat\_idemp}}2
133%       {o_continuous_relation_of_continuous_relation}{{ocrel\_of\_crel}}2
134%       {o_basic_topology_of_basic_topology}{{obtop\_of\_btop}}2
135%       {basic_topology_of_basic_pair}{{btop\_of\_bp}}2
136%       {o_basic_topology_of_o_basic_pair}{{o\_bt\_of\_o\_bp}}2
137%       {^-1}{{$^{-1}$}}1
138%       {^\ -1}{{$^{-1}$}}1
139%       {\ \\sup\ -1}{{$^{-1}$}}1
140%       {\\sup\ -1}{{$^{-1}$}}1
141%       {\ \\sup-1}{{$^{-1}$}}1
142%       {\\sup-1}{{$^{-1}$}}1
143%       {...}{{$\ldots$}}1
144        ,
145tabsize=1,
146comment=[s]{(*}{*)},
147showstringspaces=true,
148emptylines=0,
149extendedchars=true,
150sensitive=false,
151captionpos=b,
152mathescape=true,
153%keywordstyle=\bfseries,
154%keywordstyle=[2]\bfseries,
155%keywordstyle=[3]\bfseries,
156%backgroundcolor=\color{gray},
157frame=tblr,
158%frameround=tttt,
159columns=flexible,
160basicstyle=\footnotesize\tt,
161}
162
Note: See TracBrowser for help on using the repository browser.