
\RequirePackage{listings}
\RequirePackage{amssymb}
\RequirePackage{xcolor}
\RequirePackage{bold-extra}

\definecolor{thegraygray}{rgb}{0.5,0.5,0.5}

\lstdefinelanguage{why3}
{
basicstyle=\ttfamily,%
morekeywords=[1]{predicate,constant,function,goal,type,use,scope,as,%
import,theory,end,module,in,syntax,old,%
mutable,invariant,model,requires,ensures,raises,returns,reads,writes,diverges,%
variant,let,val,while,for,loop,abstract,private,any,assume,check,assert,%
begin,rec,clone,if,then,else,ghost,true,false,do,done,try,raise,absurd,%
axiom,lemma,export,forall,exists,match,with,and,inductive,coinductive,fun},%
%keywordstyle=[1]{\color{thered}},%
keywordstyle=[1]{\bfseries},%
otherkeywords={},%
commentstyle=\itshape\color{thegraygray},%
columns=[l]fullflexible,%
sensitive=true,%
morecomment=[s]{(*}{*)},%
escapeinside={*?}{?*},%
keepspaces=true,
literate=%
}

\lstnewenvironment{why3}{\lstset{language=why3}}{}
\lstnewenvironment{why3small}
{\lstset{language=why3,basicstyle=\ttfamily\footnotesize}}{}


\lstdefinelanguage{mli}
{
basicstyle=\ttfamily,%
morekeywords=[1]{predicate,constant,function,goal,type,use,%
import,theory,end,module,in,syntax,old,%
mutable,invariant,model,requires,ensures,raises,returns,reads,writes,diverges,%
variant,let,val,while,for,loop,abstract,private,any,assume,check,assert,%
begin,rec,clone,if,then,else,ghost,true,false,do,done,try,raise,absurd,%
axiom,lemma,export,forall,exists,match,with,and,inductive,coinductive,fun,%
ephemeral,modifies,checks},%
%keywordstyle=[1]{\color{thered}},%
keywordstyle=[1]{\bfseries},%
otherkeywords={},%
commentstyle=\itshape\color{thegraygray},%
columns=[l]fullflexible,%
sensitive=true,%
escapeinside={*?}{?*},%
morecomment=[s]{(**}{*)},%
keepspaces=true,
literate=%
}

\lstnewenvironment{mli}{\lstset{language=mli}}{}
\lstnewenvironment{mlismall}
{\lstset{language=mli,basicstyle=\ttfamily\footnotesize}}{}


\lstnewenvironment{C}
{\lstset{language=C,basicstyle=\ttfamily,%
columns=fullflexible,keepspaces=true,%
%keywordstyle=[1]{\color{thered}},%
keywordstyle=[1]{\bfseries},%
morekeywords=[1]{assert,uint32_t}}}{}

