1 <?xml version="1.0" encoding="UTF-8"?>
2 <language id="grafite" _name="grafite" version="2.0" _section="Sources">
4 <property name="mimetypes">text/x-matita</property>
5 <property name="globs">*.ma</property>
6 <property name="block-comment-start">(*</property>
7 <property name="block-comment-end">*)</property>
11 <style id="comment" _name="Comment" map-to="def:comment"/>
12 <style id="string" _name="String" map-to="def:string"/>
13 <style id="escape" _name="Escape" map-to="def:string"/>
14 <style id="keyword" _name="Keyword" map-to="def:keyword"/>
15 <style id="type" _name="Data Type" map-to="def:type"/>
16 <style id="latex" _name="LaTeX Escaped" map-to="def:special-char"/>
17 <style id="macros" _name="Macros" map-to="def:keyword"/>
18 <style id="tinycals" _name="Tinycals" map-to="def:keyword"/>
19 <style id="quantifiers" _name="Quantifiers" map-to="def:type"/>
23 <define-regex id="char-esc">\\"|[0-9a-zA-Z]</define-regex>
24 <context id="escape-seq" style-ref="escape">
25 <match>\%{char-esc}</match>
27 <!-- here's the main context -->
28 <context id="grafite">
30 <context id="comment" style-ref="comment">
34 <context ref="string"/>
35 <context id="comment-in-comment" style-ref="comment">
39 <context ref="string"/>
40 <context ref="comment-in-comment"/>
41 <context ref="def:in-comment:*"/>
44 <context ref="def:in-comment:*"/>
47 <context id="string" style-ref="string">
51 <context ref="escape-seq"/>
54 <context id="character-constant" style-ref="string">
55 <match>('\%{char-esc}')|('[^\\']')</match>
57 <context id="latex" style-ref="latex">
59 <keyword>def</keyword>
60 <keyword>forall</keyword>
61 <keyword>lambda</keyword>
63 <keyword>exists</keyword>
64 <keyword>Rightarrow</keyword>
65 <keyword>Assign</keyword>
66 <keyword>land</keyword>
67 <keyword>lor</keyword>
68 <keyword>lnot</keyword>
69 <keyword>liff</keyword>
70 <keyword>subst</keyword>
71 <keyword>vdash</keyword>
72 <keyword>iforall</keyword>
73 <keyword>iexists</keyword>
75 <!-- Flow control & common keywords -->
76 <context id="keywords" style-ref="keyword">
79 <keyword>implied</keyword>
82 <keyword>theorem</keyword>
83 <keyword>record</keyword>
84 <keyword>definition</keyword>
85 <keyword>inductive</keyword>
86 <keyword>coinductive</keyword>
87 <keyword>fact</keyword>
88 <keyword>lemma</keyword>
89 <keyword>remark</keyword>
90 <keyword>axiom</keyword>
93 <keyword>apply</keyword>
94 <keyword>applyS</keyword>
95 <keyword>cases</keyword>
96 <keyword>letin</keyword>
97 <keyword>auto</keyword>
98 <keyword>elim</keyword>
99 <keyword>whd</keyword>
100 <keyword>normalize</keyword>
101 <keyword>assumption</keyword>
102 <keyword>generalize</keyword>
103 <keyword>change</keyword>
104 <keyword>rewrite</keyword>
105 <keyword>cut</keyword>
106 <keyword>inversion</keyword>
107 <keyword>lapply</keyword>
108 <keyword>destruct</keyword>
109 <keyword>assume</keyword>
110 <keyword>suppose</keyword>
111 <keyword>that</keyword>
112 <keyword>is</keyword>
113 <keyword>equivalent</keyword>
114 <keyword>to</keyword>
115 <keyword>we</keyword>
116 <keyword>need</keyword>
117 <keyword>prove</keyword>
118 <keyword>or</keyword>
119 <keyword>equivalently</keyword>
120 <keyword>by</keyword>
121 <keyword>done</keyword>
122 <keyword>proved</keyword>
123 <keyword>have</keyword>
124 <keyword>such</keyword>
125 <keyword>the</keyword>
126 <keyword>thesis</keyword>
127 <keyword>becomes</keyword>
128 <keyword>conclude</keyword>
129 <keyword>obtain</keyword>
130 <keyword>proceed</keyword>
131 <keyword>induction</keyword>
132 <keyword>case</keyword>
133 <keyword>hypothesis</keyword>
134 <keyword>know</keyword>
137 <keyword>alias</keyword>
138 <keyword>and</keyword>
139 <keyword>as</keyword>
140 <keyword>associative</keyword>
141 <keyword>coercion</keyword>
142 <keyword>prefer</keyword>
143 <keyword>nocomposites</keyword>
144 <keyword>coinductive</keyword>
145 <keyword>constraint</keyword>
146 <keyword>corec</keyword>
147 <keyword>cyclic</keyword>
148 <keyword>default</keyword>
149 <keyword>discriminator</keyword>
150 <keyword>for</keyword>
151 <keyword>id</keyword>
152 <keyword>include</keyword>
153 <keyword>include'</keyword>
154 <keyword>inductive</keyword>
155 <keyword>inverter</keyword>
156 <keyword>in</keyword>
157 <keyword>interpretation</keyword>
158 <keyword>left</keyword>
159 <keyword>let</keyword>
160 <keyword>match</keyword>
161 <keyword>names</keyword>
162 <keyword>non</keyword>
163 <keyword>notation</keyword>
164 <keyword>on</keyword>
165 <keyword>precedence</keyword>
166 <keyword>qed</keyword>
167 <keyword>defined</keyword>
168 <keyword>rec</keyword>
169 <keyword>record</keyword>
170 <keyword>return</keyword>
171 <keyword>right</keyword>
172 <keyword>source</keyword>
173 <keyword>symbol</keyword>
174 <keyword>to</keyword>
175 <keyword>universe</keyword>
176 <keyword>using</keyword>
177 <keyword>with</keyword>
181 <keyword>unification</keyword>
182 <keyword>hint</keyword>
183 <keyword>coercion</keyword>
184 <keyword>inverter</keyword>
185 <keyword>qed</keyword>
188 <keyword>check</keyword>
189 <keyword>eval</keyword>
190 <keyword>hint</keyword>
191 <keyword>set</keyword>
192 <keyword>auto</keyword>
193 <keyword>nodefaults</keyword>
194 <keyword>coercions</keyword>
195 <keyword>comments</keyword>
196 <keyword>debug</keyword>
199 <keyword>try</keyword>
200 <keyword>solve</keyword>
201 <keyword>do</keyword>
202 <keyword>repeat</keyword>
203 <keyword>first</keyword>
204 <keyword>focus</keyword>
205 <keyword>unfocus</keyword>
206 <keyword>progress</keyword>
207 <keyword>skip</keyword>
209 <context id="types" style-ref="type">
211 <keyword>Prop</keyword>
212 <keyword>Type[0]</keyword>
213 <keyword>CProp[0]</keyword>
214 <keyword>Type[1]</keyword>
215 <keyword>CProp[1]</keyword>
216 <keyword>Type[2]</keyword>
217 <keyword>CProp[2]</keyword>
219 <context id="quantifiers" style-ref="quantifiers">
221 <match>∀|∃|λ|=|→|⇒|…|≝|≡|\?</match>
223 <context id="tinycals" style-ref="tinycals">
224 <match>\[|\||\]|\{|\}|>|//|<|@|\$|#|\\\\|;|\.|:>|:|-</match>