[2052] | 1 | \lstdefinelanguage{grafite} { |
---|
| 2 | mathescape=true, |
---|
| 3 | texcl=false, |
---|
| 4 | keywords={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}, |
---|
| 9 | morekeywords={[2]include}, |
---|
| 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 | tabsize=1, |
---|
| 145 | comment=[s]{(*}{*)}, |
---|
| 146 | showstringspaces=true, |
---|
| 147 | emptylines=0, |
---|
| 148 | extendedchars=true, |
---|
| 149 | sensitive=false, |
---|
| 150 | captionpos=b, |
---|
| 151 | mathescape=true, |
---|
| 152 | keywordstyle=\bfseries, |
---|
| 153 | keywordstyle=[2]\bfseries, |
---|
| 154 | keywordstyle=[3]\bfseries, |
---|
| 155 | %backgroundcolor=\color{gray}, |
---|
| 156 | frame=tblr, |
---|
| 157 | %frameround=tttt, |
---|
| 158 | columns=flexible, |
---|
| 159 | basicstyle=\footnotesize\tt, |
---|
| 160 | } |
---|
| 161 | |
---|