1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
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,
}
|
