helm/software/matita/matita.lang

   1 <?xml version="1.0" encoding="UTF-8"?>
   2 <language id="grafite" _name="grafite" version="2.0" _section="Sources">
   3   <metadata>
   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>
   8   </metadata>
   9
  10   <styles>
  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"/>
  20   </styles>
  21
  22   <definitions>
  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>
  26     </context>
  27     <!-- here's the main context -->
  28     <context id="grafite">
  29       <include>
  30         <context id="comment" style-ref="comment">
  31           <start>\(\*</start>
  32           <end>\*\)</end>
  33           <include>
  34             <context ref="string"/>
  35             <context id="comment-in-comment" style-ref="comment">
  36               <start>\(\*</start>
  37               <end>\*\)</end>
  38               <include>
  39                 <context ref="string"/>
  40                 <context ref="comment-in-comment"/>
  41                 <context ref="def:in-comment:*"/>
  42               </include>
  43             </context>
  44             <context ref="def:in-comment:*"/>
  45           </include>
  46         </context>
  47         <context id="string" style-ref="string">
  48           <start>"</start>
  49           <end>"</end>
  50           <include>
  51             <context ref="escape-seq"/>
  52           </include>
  53         </context>
  54         <context id="character-constant" style-ref="string">
  55           <match>('\%{char-esc}')|('[^\\']')</match>
  56         </context>
  57         <context id="whelp_macros" style-ref="macros">
  58          <prefix>whelp *</prefix>
  59          <keyword>elim</keyword>
  60          <keyword>hint</keyword>
  61          <keyword>instance</keyword>
  62          <keyword>locate</keyword>
  63          <keyword>match</keyword>
  64         </context>
  65         <context id="latex" style-ref="latex">
  66          <prefix>\\</prefix>
  67          <keyword>def</keyword>
  68          <keyword>forall</keyword>
  69          <keyword>lambda</keyword>
  70          <keyword>to</keyword>
  71          <keyword>exists</keyword>
  72          <keyword>Rightarrow</keyword>
  73          <keyword>Assign</keyword>
  74          <keyword>land</keyword>
  75          <keyword>lor</keyword>
  76          <keyword>lnot</keyword>
  77          <keyword>liff</keyword>
  78          <keyword>subst</keyword>
  79          <keyword>vdash</keyword>
  80          <keyword>iforall</keyword>
  81          <keyword>iexists</keyword>
  82         </context>
  83         <!-- Flow control & common keywords -->
  84         <context id="keywords" style-ref="keyword">
  85          <!-- objects -->
  86          <keyword>theorem</keyword>
  87          <keyword>definition</keyword>
  88          <keyword>lemma</keyword>
  89          <keyword>fact</keyword>
  90          <keyword>remark</keyword>
  91          <keyword>variant</keyword>
  92          <keyword>axiom</keyword>
  93
  94          <!-- nobjects -->
  95          <keyword>ntheorem</keyword>
  96          <keyword>nrecord</keyword>
  97          <keyword>ndefinition</keyword>
  98          <keyword>ninductive</keyword>
  99          <keyword>ncoinductive</keyword>
 100          <keyword>nlet</keyword>
 101          <keyword>nlemma</keyword>
 102          <keyword>nremark</keyword>
 103          <keyword>naxiom</keyword>
 104
 105          <!-- tactics -->
 106          <keyword>absurd</keyword>
 107          <keyword>apply</keyword>
 108          <keyword>applyP</keyword>
 109          <keyword>assumption</keyword>
 110          <keyword>autobatch</keyword>
 111          <keyword>cases</keyword>
 112          <keyword>clear</keyword>
 113          <keyword>clearbody</keyword>
 114          <keyword>change</keyword>
 115          <keyword>compose</keyword>
 116          <keyword>constructor</keyword>
 117          <keyword>contradiction</keyword>
 118          <keyword>cut</keyword>
 119          <keyword>decompose</keyword>
 120          <keyword>destruct</keyword>
 121          <keyword>elim</keyword>
 122          <keyword>elimType</keyword>
 123          <keyword>exact</keyword>
 124          <keyword>exists</keyword>
 125          <keyword>fail</keyword>
 126          <keyword>fold</keyword>
 127          <keyword>fourier</keyword>
 128          <keyword>fwd</keyword>
 129          <keyword>generalize</keyword>
 130          <keyword>id</keyword>
 131          <keyword>intro</keyword>
 132          <keyword>intros</keyword>
 133          <keyword>inversion</keyword>
 134          <keyword>lapply</keyword>
 135          <keyword>linear</keyword>
 136          <keyword>left</keyword>
 137          <keyword>letin</keyword>
 138          <keyword>normalize</keyword>
 139          <keyword>reflexivity</keyword>
 140          <keyword>replace</keyword>
 141          <keyword>rewrite</keyword>
 142          <keyword>ring</keyword>
 143          <keyword>right</keyword>
 144          <keyword>symmetry</keyword>
 145          <keyword>simplify</keyword>
 146          <keyword>split</keyword>
 147          <keyword>to</keyword>
 148          <keyword>transitivity</keyword>
 149          <keyword>unfold</keyword>
 150          <keyword>whd</keyword>
 151          <keyword>assume</keyword>
 152          <keyword>suppose</keyword>
 153          <keyword>by</keyword>
 154          <keyword>is</keyword>
 155          <keyword>or</keyword>
 156          <keyword>equivalent</keyword>
 157          <keyword>equivalently</keyword>
 158          <keyword>we</keyword>
 159          <keyword>prove</keyword>
 160          <keyword>proved</keyword>
 161          <keyword>need</keyword>
 162          <keyword>proceed</keyword>
 163          <keyword>induction</keyword>
 164          <keyword>inductive</keyword>
 165          <keyword>case</keyword>
 166          <keyword>base</keyword>
 167          <keyword>let</keyword>
 168          <keyword>such</keyword>
 169          <keyword>that</keyword>
 170          <keyword>by</keyword>
 171          <keyword>have</keyword>
 172          <keyword>and</keyword>
 173          <keyword>the</keyword>
 174          <keyword>thesis</keyword>
 175          <keyword>becomes</keyword>
 176          <keyword>hypothesis</keyword>
 177          <keyword>know</keyword>
 178          <keyword>case</keyword>
 179          <keyword>obtain</keyword>
 180          <keyword>conclude</keyword>
 181          <keyword>done</keyword>
 182          <keyword>rule</keyword>
 183
 184          <!-- ntactics -->
 185          <keyword>napply</keyword>
 186          <keyword>napplyS</keyword>
 187          <keyword>ncases</keyword>
 188          <keyword>nletin</keyword>
 189          <keyword>nauto</keyword>
 190          <keyword>nelim</keyword>
 191          <keyword>nwhd</keyword>
 192          <keyword>nnormalize</keyword>
 193          <keyword>nassumption</keyword>
 194          <keyword>ngeneralize</keyword>
 195          <keyword>nchange</keyword>
 196          <keyword>nrewrite</keyword>
 197          <keyword>ncut</keyword>
 198          <keyword>ninversion</keyword>
 199          <keyword>nlapply</keyword>
 200          <keyword>ndestruct</keyword>
 201
 202           <!-- commands -->
 203           <keyword>alias</keyword>
 204           <keyword>and</keyword>
 205           <keyword>as</keyword>
 206           <keyword>coercion</keyword>
 207           <keyword>prefer</keyword>
 208           <keyword>nocomposites</keyword>
 209           <keyword>coinductive</keyword>
 210           <keyword>corec</keyword>
 211           <keyword>default</keyword>
 212           <keyword>for</keyword>
 213           <keyword>include</keyword>
 214           <keyword>include'</keyword>
 215           <keyword>inductive</keyword>
 216           <keyword>inverter</keyword>
 217           <keyword>in</keyword>
 218           <keyword>interpretation</keyword>
 219           <keyword>let</keyword>
 220           <keyword>match</keyword>
 221           <keyword>names</keyword>
 222           <keyword>notation</keyword>
 223           <keyword>on</keyword>
 224           <keyword>qed</keyword>
 225           <keyword>rec</keyword>
 226           <keyword>record</keyword>
 227           <keyword>return</keyword>
 228           <keyword>source</keyword>
 229           <keyword>to</keyword>
 230           <keyword>using</keyword>
 231           <keyword>with</keyword>
 232
 233
 234           <!-- ncommands -->
 235           <keyword>unification</keyword>
 236           <keyword>hint</keyword>
 237           <keyword>ncoercion</keyword>
 238           <keyword>ninverter</keyword>
 239           <keyword>nqed</keyword>
 240
 241           <!-- macros -->
 242           <keyword>inline</keyword>
 243           <keyword>procedural</keyword>
 244           <keyword>check</keyword>
 245           <keyword>eval</keyword>
 246           <keyword>hint</keyword>
 247           <keyword>set</keyword>
 248           <keyword>auto</keyword>
 249           <keyword>nodefaults</keyword>
 250           <keyword>coercions</keyword>
 251           <keyword>comments</keyword>
 252           <keyword>debug</keyword>
 253           <keyword>cr</keyword>
 254
 255           <!-- nmacros -->
 256           <keyword>ncheck</keyword>
 257
 258           <!-- tinycals -->
 259           <keyword>try</keyword>
 260           <keyword>solve</keyword>
 261           <keyword>do</keyword>
 262           <keyword>repeat</keyword>
 263           <keyword>first</keyword>
 264           <keyword>focus</keyword>
 265           <keyword>unfocus</keyword>
 266           <keyword>progress</keyword>
 267           <keyword>skip</keyword>
 268         </context>
 269         <context id="types" style-ref="type">
 270           <!-- sorts -->
 271           <keyword>Set</keyword>
 272           <keyword>Prop</keyword>
 273           <keyword>Type</keyword>
 274           <keyword>CProp</keyword>
 275
 276           <!-- nsorts -->
 277           <keyword>Prop</keyword>
 278           <keyword>Type[0]</keyword>
 279           <keyword>CProp[0]</keyword>
 280           <keyword>Type[1]</keyword>
 281           <keyword>CProp[1]</keyword>
 282           <keyword>Type[2]</keyword>
 283           <keyword>CProp[2]</keyword>
 284         </context>
 285         <context id="quantifiers" style-ref="quantifiers">
 286           <!-- quantifiers -->
 287           <match>∀|∃|λ|=|→|⇒|…|≝|≡|\?</match>
 288         </context>
 289         <context id="tinycals" style-ref="tinycals">
 290           <match>\[|\||\]|\{|\}|@|\$|#|\\\\|;|\.|:>|:</match>
 291         </context>
 292       </include>
 293     </context>
 294   </definitions>
 295 </language>