source: Papers/jar-assembler-2015/lst-grafite.tex @ 3558

\lstdefinelanguage{grafite} {
mathescape=true,
texcl=false,
keywords={record, with, match, let, rec, corec, inductive, definition, axiom,
        qed, intro, intros, symmetry, simplify, rewrite, apply, elim, assumption,
        left, cut, cases, auto, right, coercion, split, lemma, theorem, skip, constructor, copy, from, letin, 
        by, done, we, conclude, assume, need, to, prove, unfold, return, and, check,
        notation, interpretation, lapply, repeat, try, as, clear, in, change, whd, exists},
morekeywords={[2]include},
%emph={[1]Type, Prop, nat, real}, emphstyle={[1]\textit},
% literate=     
%       {->}{{$\to$}}3          
%       {:>}{{$\mathrm{:>}$}}1          
%       {>->}{{$\mapsto$}}2             
%       {<=}{{$\leq$}}2                 
%       {>=}{{$\geq$}}2         
%       {<>}{{$\neq$}}1
%       {\\/}{{$\vee$}}1                
%       {<->}{{$\leftrightarrow$}}2
%       {FORALL\ }{{$\forall\,$}}1              
%       {EXISTS\ }{{$\exists\,$}}1
%       {ALPHA}{{$\alpha$}}1
%       {LAMBDA}{{$\lambda\,$}}1
%       {\\lambda}{{$\lambda\,$}}1
%       {LANGLE}{{$\langle$}}1
%       {RANGLE}{{$\rangle$}}1
%       {EQUIV}{{$\equiv$}}1
%       {SIGMA}{{$\Sigma$}}1
%       {PSI}{{$\Psi$}}1
%       {DOTS}{{$\ldots$}}1
%       {NOT}{{$\neg$}}1
%       {\\in}{{$\in$}}1
%       {𝟙}{{$\mathbf{1}$}}1
%       {𝟘}{{$\mathbf{0}$}}1
%       {/\\}{$\land$}1
%       {×}{{$\times\,$}}2
%       {\\x}{{$\times\,$}}2
%       {≝}{{:=}}1
%       {δ}{{$\delta$}}1
%       {λ}{{$\lambda\,$}}1
%       {≰}{{$\nleq\,$}}1
%       {∨}{{$\lor\,$}}1
%       {⋁}{{$\bigvee$}}1
%       {≈}{{$\approx\,$}}1
%       {∀}{{$\forall\,$}}1
%       {∃}{{$\exists\,$}}1
%       {⇝}{{$\leadsto\,$}}1
%       {→}{{$\rightarrow\,$}}1
%       {↔}{{$\leftrightarrow$}}1
%       {∧}{{$\land\,$}}1
%       {⋀}{{$\bigwedge$}}1
%       {≤}{{$\leq\,$}}1
%       {¬}{{$\lnot\,$}}1
%       {≪}{{$\ll\,$}}1
%       {≫}{{$\gg\,$}}1
%       {⇒}{{$\,\Rightarrow\,\,$}}2
%       {=>}{{$\,\Rightarrow\,\,$}}2
%       {⇒_0}{{$\,\Rightarrow_0\,\,$}}2
%       {=>_0}{{$\,\Rightarrow_0\,\,$}}2
%       {⇒_1}{{$\,\Rightarrow_1\,$}}1
%       {⇒_1.}{{$\,\Rightarrow_1\,$}}1
%       {⇒_\\r1}{{$\,\Rightarrow_1^{r}\,$}}1
%       {⇒_\\r2}{{$\,\Rightarrow_2^{r}\,$}}1
%       {=>_1}{{$\,\Rightarrow_1\,$}}1
%       {⇒_2}{{$\,\Rightarrow_2\,$}}1
%       {⇒_\\o2}{{$\,\Rightarrow_2^o\,$}}1
%       {⇒_\\c2}{{$\,\Rightarrow_2^c\,$}}1
%       {⇒_\\c3}{{$\,\Rightarrow_3^c\,$}}1
%       {⇒_\\obp2}{{$\,\Rightarrow_2^{obp}\,$}}1
%       {⇒_\\bp1}{{$\,\Rightarrow_1^{bp}\,$}}1
%       {⇒_\\bp2}{{$\,\Rightarrow_2^{bp}\,$}}1
%       {⇒_\\obt2}{{$\,\Rightarrow_2^{obt}\,$}}1
%       {⇒_2.}{{$\,\Rightarrow_2\,$}}1
%       {=>_2}{{$\,\Rightarrow_2\,$}}1
%       {=_1}{{$=$}}1
%       {=_2}{{$=$}}1
%       {⊢}{{$\vdash$}}1
%       {⊩}{{$\Vdash\,$}}2
%       {≬}{{$\between$}}2
%       {><}{{$>\!\!\!\!\!<\,$}}2
%       {⎻}{{$^-$}}1
%       {⎻*}{{$^{-*}$}}1
%       {\\sup\ ⎻}{{$\!^-\,$}}1
%       {\\sup\ ⎻*}{{$\!^{-*}\,$}}1
%       {\\sup\ *}{{$\!^{*}\,$}}1
%       {^*}{{$\!^{*}\,$}}1
%       {F*}{{F$^*$}}1
%       {G*}{{G$^*$}}1
%       {∘}{{$\circ\;$}}2
%       {Ω}{{$\Omega$}}1
%       {Ω^carrbt}{{$\Omega^{\mbox{carrbt}}$}}1
%       {Ω^A}{{$\Omega^A$}}1
%       {Ω^C}{{$\Omega^C$}}1
%       {Ω^U}{{$\Omega^U$}}1
%       {Ω^V}{{$\Omega^V$}}1
%       {Ω^X}{{$\Omega^X$}}1
%       {Ω^s}{{$\Omega^s$}}1
%       {‡}{{$\ddagger$}}1
%       {†}{{$\dagger$}}1
%       {⊆}{{$\subseteq\,$}}2
%       {♮}{{$\natural$}}1
%       {∩}{{$\cap$}}2
%       {∪}{{$\cup$}}2
%       {⋂}{{$\bigcap$}}2
%       {⋃}{{$\bigcup$}}2
%       {∈}{{$\in\,$}}2
%       {⎽o}{{$_o$}}1
%       {⎽f}{{$_f$}}1
%       {'\ \\sub\\c}{{'$\!_c$}}1
%       {\ \\sub\\c}{{$_c$}}1
%       {'\\sub\\c}{{'$\!_c$}}1
%       {\\sub\\c}{{$_c$}}1
%       {'\ \\sub\\f}{{'$\!_f$}}1
%       {\ \\sub\\f}{{$_f$}}1
%       {'\\sub\\f}{{'$\!_f$}}1
%       {\\sub\\f}{{$_f$}}1
%       {\\sup\ (form\ o)}{{$^{o_f}$}}1
%       {\\sup\ (concr\ o)}{{$^{o_c}$}}1
%       {(form\ o)}{{o$_f~$}}2
%       {(concr\ o)}{{o$_c~$}}2
%       {form\ o}{{o$_f~$}}2
%       {concr\ o}{{o$_c~$}}2
%       {Ω^(form\ o)}{{$\Omega^{o_f}~$}}2
%       {Ω^(concr\ o)}{{$\Omega^{o_c}~$}}2
%       {◊⎽t}{{$\Diamond_t$}}1
%       {□⎽t}{{$\boxempty_t$}}1
%       {⎽⇒}{{$_\Rightarrow$}}1
%       {o_operator_of_operator}{{o\_op\_of\_op}}2
%       {o_saturation_expansive}{{o\_sat\_expa}}2
%       {o_saturation_monotone}{{o\_sat\_monot}}2
%       {o_saturation_idempotent}{{o\_sat\_idemp}}2
%       {o_continuous_relation_of_continuous_relation}{{ocrel\_of\_crel}}2
%       {o_basic_topology_of_basic_topology}{{obtop\_of\_btop}}2
%       {basic_topology_of_basic_pair}{{btop\_of\_bp}}2
%       {o_basic_topology_of_o_basic_pair}{{o\_bt\_of\_o\_bp}}2
%       {^-1}{{$^{-1}$}}1
%       {^\ -1}{{$^{-1}$}}1
%       {\ \\sup\ -1}{{$^{-1}$}}1
%       {\\sup\ -1}{{$^{-1}$}}1
%       {\ \\sup-1}{{$^{-1}$}}1
%       {\\sup-1}{{$^{-1}$}}1
%       {...}{{$\ldots$}}1
        ,
tabsize=1,
comment=[s]{(*}{*)},
showstringspaces=true,
emptylines=0,
extendedchars=true,
sensitive=false,
captionpos=b,
mathescape=true,
keywordstyle=\bfseries,
keywordstyle=[2]\bfseries,
keywordstyle=[3]\bfseries,
%backgroundcolor=\color{gray},
frame=tblr,
%frameround=tttt,
columns=flexible,
basicstyle=\footnotesize\tt,
}