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

\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,
}