diff options
Diffstat (limited to 'doc/refman/coq-listing.tex')
| -rw-r--r-- | doc/refman/coq-listing.tex | 152 |
1 files changed, 152 insertions, 0 deletions
diff --git a/doc/refman/coq-listing.tex b/doc/refman/coq-listing.tex new file mode 100644 index 0000000000..c69c3b1b81 --- /dev/null +++ b/doc/refman/coq-listing.tex @@ -0,0 +1,152 @@ +%======================================================================= +% Listings LaTeX package style for Gallina + SSReflect (Assia Mahboubi 2007) + +\lstdefinelanguage{SSR} { + +% Anything betweeen $ becomes LaTeX math mode +mathescape=true, +% Comments may or not include Latex commands +texcl=false, + + +% Vernacular commands +morekeywords=[1]{ +From, Section, Module, End, Require, Import, Export, Defensive, Function, +Variable, Variables, Parameter, Parameters, Axiom, Hypothesis, Hypotheses, +Notation, Local, Tactic, Reserved, Scope, Open, Close, Bind, Delimit, +Definition, Let, Ltac, Fixpoint, CoFixpoint, Add, Morphism, Relation, +Implicit, Arguments, Set, Unset, Contextual, Strict, Prenex, Implicits, +Inductive, CoInductive, Record, Structure, Canonical, Coercion, +Theorem, Lemma, Corollary, Proposition, Fact, Remark, Example, +Proof, Goal, Save, Qed, Defined, Hint, Resolve, Rewrite, View, +Search, Show, Print, Printing, All, Graph, Projections, inside, +outside, Locate, Maximal}, + +% Gallina +morekeywords=[2]{forall, exists, exists2, fun, fix, cofix, struct, + match, with, end, as, in, return, let, if, is, then, else, + for, of, nosimpl}, + +% Sorts +morekeywords=[3]{Type, Prop}, + +% Various tactics, some are std Coq subsumed by ssr, for the manual purpose +morekeywords=[4]{ + pose, set, move, case, elim, apply, clear, + hnf, intro, intros, generalize, rename, pattern, after, + destruct, induction, using, refine, inversion, injection, + rewrite, congr, unlock, compute, ring, field, + replace, fold, unfold, change, cutrewrite, simpl, + have, gen, generally, suff, wlog, suffices, without, loss, nat_norm, + assert, cut, trivial, revert, bool_congr, nat_congr, abstract, + symmetry, transitivity, auto, split, left, right, autorewrite}, + +% Terminators +morekeywords=[5]{ + by, done, exact, reflexivity, tauto, romega, omega, + assumption, solve, contradiction, discriminate}, + + +% Control +morekeywords=[6]{do, last, first, try, idtac, repeat}, + +% Various symbols +% For the ssr manual we turn off the prettyprint of formulas +% literate= +% {->}{{$\rightarrow\,$}}2 +% {->}{{\tt ->}}3 +% {<-}{{$\leftarrow\,$}}2 +% {<-}{{\tt <-}}2 +% {>->}{{$\mapsto$}}3 +% {<=}{{$\leq$}}1 +% {>=}{{$\geq$}}1 +% {<>}{{$\neq$}}1 +% {/\\}{{$\wedge$}}2 +% {\\/}{{$\vee$}}2 +% {<->}{{$\leftrightarrow\;$}}3 +% {<=>}{{$\Leftrightarrow\;$}}3 +% {:nat}{{$~\in\mathbb{N}$}}3 +% {fforall\ }{{$\forall_f\,$}}1 +% {forall\ }{{$\forall\,$}}1 +% {exists\ }{{$\exists\,$}}1 +% {negb}{{$\neg$}}1 +% {spp}{{:*:\,}}1 +% {~}{{$\sim$}}1 +% {\\in}{{$\in\;$}}1 +% {/\\}{$\land\,$}1 +% {:*:}{{$*$}}2 +% {=>}{{$\,\Rightarrow\ $}}1 +% {=>}{{\tt =>}}2 +% {:=}{{{\tt:=}\,\,}}2 +% {==}{{$\equiv$}\,}2 +% {!=}{{$\neq$}\,}2 +% {^-1}{{$^{-1}$}}1 +% {elt'}{elt'}1 +% {=}{{\tt=}\,\,}2 +% {+}{{\tt+}\,\,}2, +literate= + {isn't }{{{\ttfamily\color{dkgreen} isn't }}}1, + +% Comments delimiters, we do turn this off for the manual +%comment=[s]{(*}{*)}, + +% Spaces are not displayed as a special character +showstringspaces=false, + +% String delimiters +morestring=[b]", +morestring=[d]", + +% Size of tabulations +tabsize=3, + +% Enables ASCII chars 128 to 255 +extendedchars=true, + +% Case sensitivity +sensitive=true, + +% Automatic breaking of long lines +breaklines=true, + +% Default style fors listings +basicstyle=\ttfamily, + +% Position of captions is bottom +captionpos=b, + +% Full flexible columns +columns=[l]fullflexible, + +% Style for (listings') identifiers +identifierstyle={\ttfamily\color{black}}, +% Note : highlighting of Coq identifiers is done through a new +% delimiter definition through an lstset at the begining of the +% document. Don't know how to do better. + +% Style for declaration keywords +keywordstyle=[1]{\ttfamily\color{dkviolet}}, + +% Style for gallina keywords +keywordstyle=[2]{\ttfamily\color{dkgreen}}, + +% Style for sorts keywords +keywordstyle=[3]{\ttfamily\color{lightblue}}, + +% Style for tactics keywords +keywordstyle=[4]{\ttfamily\color{dkblue}}, + +% Style for terminators keywords +keywordstyle=[5]{\ttfamily\color{red}}, + + +%Style for iterators +keywordstyle=[6]{\ttfamily\color{dkpink}}, + +% Style for strings +stringstyle=\ttfamily, + +% Style for comments +commentstyle=\rmfamily, + +} |