1 | \lstdefinelanguage{grafite} { |
---|
2 | mathescape=true, |
---|
3 | texcl=false, |
---|
4 | keywords={include}, |
---|
5 | morekeywords={record, with, match, let, rec, corec, inductive, definition, axiom, |
---|
6 | qed, intro, intros, symmetry, simplify, rewrite, apply, elim, assumption, |
---|
7 | left, cut, cases, auto, right, coercion, split, lemma, theorem, skip, constructor, copy, from, letin, |
---|
8 | by, done, we, conclude, assume, need, to, prove, unfold, return, and, check, |
---|
9 | notation, interpretation, lapply, repeat, try, as, clear, in, change, whd, exists}, |
---|
10 | %emph={[1]Type, Prop, nat, real}, emphstyle={[1]\textit}, |
---|
11 | literate= |
---|
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 | , |
---|
144 | comment=[s]{(*}{*)}, |
---|
145 | showstringspaces=true, |
---|
146 | emptylines=0, |
---|
147 | extendedchars=true, |
---|
148 | sensitive=false, |
---|
149 | captionpos=b, |
---|
150 | mathescape=true, |
---|
151 | %backgroundcolor=\color{gray}, |
---|
152 | frame=tblr, |
---|
153 | %frameround=tttt, |
---|
154 | columns=flexible, |
---|
155 | basicstyle=\footnotesize\tt, |
---|
156 | } |
---|
157 | |
---|