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

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

\lstdefinelanguage{gospel}
{
basicstyle=\ttfamily,%
morekeywords=[1]{predicate,constant,consumes,function,goal,type,use,%
import,theory,end,module,in,syntax,old,scope,functor,struct,sig,to,%
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},%
keywordstyle=[1]{\color{thered}},%
%keywordstyle=\bfseries,%
otherkeywords={},%
commentstyle=\itshape\color{thegraygray},%
columns=[l]fullflexible,%
sensitive=true,%
escapeinside={*?}{?*},%
keepspaces=true,
literate=%
 {-}{\raisebox{0.08em}{-}}{1}% for nicer ->
% {'a}{$\alpha$}{1}%
% {'b}{$\beta$}{1}%
% {<}{$<$}{1}%
% {>}{$>$}{1}%
% {<=}{$\le$}{1}%
% {>=}{$\ge$}{1}%
% {<>}{$\ne$}{1}%
% {/\\}{$\land$}{1}%
% {\\/}{ $\lor$ }{3}%
% {\ or(}{ $\lor$(}{3}%
% {not\ }{$\lnot$ }{2}%
% {not(}{$\lnot$(}{2}%
% {+->}{\texttt{+->}}{3}%
% {+->}{$\mapsto$}{2}%
% {-->}{\texttt{-\relax->}}{3}%
% {-->}{$\longrightarrow$}{2}%
% {->}{$\rightarrow$}{2}%
% {<-}{$\leftarrow$}{2}%
% {<->}{$\leftrightarrow$}{2}%
}

\lstnewenvironment{gospel}{\lstset{language=gospel,aboveskip=5pt,belowskip=5pt}}{}
\lstnewenvironment{gospelsmall}
{\lstset{language=gospel,basicstyle=\ttfamily\footnotesize}}{}

\def\gosp{\lstinline[language=gospel, basicstyle=\ttfamily]} %normalsize
\def\gosprm{\lstinline[language=gospel, basicstyle=\normalsize]}
\let\of\gosp
