source: LTS/DICE2014/lst-grafite.tex @ 3498

\lstdefinelanguage{grafite} {
mathescape=true,
texcl=false,
keywords={include, set},
morekeywords={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,
        by, done, we, conclude, assume, need, to, prove, unfold, return, and,
        notation, interpretation, lapply, repeat, try, as, clear, in},
%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
        {LANGLE}{{$\langle$}}1
        {RANGLE}{{$\rangle$}}1
        {EQUIV}{{$\equiv$}}1
        {SIGMA}{{$\Sigma$}}1
        {PSI}{{$\Psi$}}1
        {DOTS}{{$\ldots$}}1
        {NOT}{{$\neg$}}1
        {\\in}{{$\in$}}1
        {/\\}{$\land$}1
        {=>}{{$\,\Rightarrow\,$}}1
        {≝}{{:=}}1
        {δ}{{$\delta$}}1
        {λ}{{$\lambda\,$}}1
        {≰}{{$\nleq\,$}}1
        {∨}{{$\lor\,$}}1
        {≈}{{$\approx\,$}}1
        {∀}{{$\forall\,$}}1
        {∃}{{$\exists\,$}}1
        {⇝}{{$\leadsto\,$}}1
        {→}{{$\rightarrow\,$}}1
        {∧}{{$\land\,$}}1
        {≤}{{$\leq\,$}}1
        {¬}{{$\lnot\,$}}1
        {≪}{{$\ll\,$}}1
        {≫}{{$\gg\,$}}1
        {⇒}{{$\,\Rightarrow$}}1
        {⊢}{{$\vdash$}}1
        {...}{{$\ldots$}}1
        {ℕ}{{$\mathbb{N}$}}1
        {Σ}{{$\Sigma$}}1
        {Ⓧ}{{$\bigotimes$}}1
        {…}{{$\ldots$}}1
        {≠}{{$\neq$}}1
        {〈}{{$\langle$}}1
        {〉}{{$\rangle$}}1 
        ,
comment=[s]{(*}{*)},
showstringspaces=true,
extendedchars=true,
sensitive=false,
captionpos=b,
mathescape=true,
%backgroundcolor=\color{gray},
frame=tblr,
frameround=tttt,
columns=flexible,
basicstyle=\small,
}