helm/meta_style/set.xml

   1 <!DOCTYPE OpList SYSTEM "operator.dtd">
   2
   3 <OpList xmlns:m="http://www.w3.org/1998/Math/MathML">
   4
   5 <import href="modeset.xsl"/>
   6
   7 <Operator
   8  name  = "IN"
   9  uri   = "cic:/Coq/Sets/Ensembles/In.con"
  10  cook  = "true"
  11  arity = "2">
  12         <mapp>
  13                 <mop tag="in"/>
  14                 <param id="2"/>
  15                 <param id="1" mode="set"/>
  16         </mapp>
  17 </Operator>
  18
  19 <NotOperator
  20  name  = "NOT IN"
  21  uri   = "cic:/Coq/Sets/Ensembles/In.con"
  22  cook  = "true"
  23  arity = "2">
  24         <mapp>
  25                 <m:notin/>
  26                 <param id="2"/>
  27                 <param id="1" mode="set"/>
  28         </mapp>
  29 </NotOperator>
  30
  31 <Operator
  32  name  = "EMPTY SET"
  33  uri   = "cic:/Coq/Sets/Ensembles/Empty_set.ind"
  34  cook  = "true"
  35  arity = "1">
  36                 <mapp>
  37                         <m:in definitionURL="cic:/Coq/Sets/Ensembles/In.con"/>
  38                         <param id="1"/>
  39                         <mop tag="set" helm:xref="$APP-ID"/>
  40                 </mapp>
  41 </Operator>
  42
  43 <Operator
  44  name  = "EMPTY SET"
  45  uri   = "cic:/Coq/Sets/Ensembles/Empty_set.ind"
  46  cook  = "true">
  47         <mop tag="set" helm:xref="$APP-ID"/>
  48 </Operator>
  49
  50
  51 <Operator
  52  name  = "SINGLETON"
  53  uri   = "cic:/Coq/Sets/Ensembles/Singleton.ind"
  54  cook  = "true"
  55  arity = "1">
  56                 <mop tag="set" helm:xref="$APP-ID">
  57                         <param id="1"/>
  58                 </mop>
  59 </Operator>
  60
  61 <Operator
  62  name  = "SINGLETON"
  63  uri   = "cic:/Coq/Sets/Ensembles/Singleton.ind"
  64  cook  = "true"
  65  arity = "2">
  66                 <mapp>
  67                         <m:in definitionURL="cic:/Coq/Sets/Ensembles/In.con"/>
  68                         <param id="2"/>
  69                         <m:set definitionURL="$OP-URI">
  70                                 <param id="1"/>
  71                         </m:set>
  72                 </mapp>
  73 </Operator>
  74
  75 <Operator
  76  name  = "COUPLE"
  77  uri   = "cic:/Coq/Sets/Ensembles/Couple.ind"
  78  cook  = "true"
  79  arity = "2">
  80                 <mop tag="set" helm:xref="$APP-ID">
  81                         <param id="1"/>
  82                         <param id="2"/>
  83                 </mop>
  84 </Operator>
  85
  86 <Operator
  87  name  = "COUPLE"
  88  uri   = "cic:/Coq/Sets/Ensembles/Couple.ind"
  89  cook  = "true"
  90  arity = "3">
  91                 <mapp>
  92                         <m:in definitionURL="cic:/Coq/Sets/Ensembles/In.con"/>
  93                         <param id="3"/>
  94                         <m:set definitionURL="$OP-URI">
  95                                 <param id="1"/>
  96                                 <param id="2"/>
  97                         </m:set>
  98                 </mapp>
  99 </Operator>
 100
 101 <Operator
 102  name  = "TRIPLE"
 103  uri   = "cic:/Coq/Sets/Ensembles/Triple.ind"
 104  cook  = "true"
 105  arity = "3">
 106                 <mop tag="set">
 107                         <param id="1"/>
 108                         <param id="2"/>
 109                         <param id="3"/>
 110                 </mop>
 111 </Operator>
 112
 113 <Operator
 114  name  = "TRIPLE"
 115  uri   = "cic:/Coq/Sets/Ensembles/Triple.ind"
 116  cook  = "true"
 117  arity = "4">
 118                 <mapp>
 119                         <m:in definitionURL="cic:/Coq/Sets/Ensembles/In.con"/>
 120                         <param id="4"/>
 121                         <m:set definitionURL="$OP-URI">
 122                                 <param id="1"/>
 123                                 <param id="2"/>
 124                                 <param id="3"/>
 125                         </m:set>
 126                 </mapp>
 127 </Operator>
 128
 129 <Operator
 130  name  = "INTERSECTION"
 131  uri   = "cic:/Coq/Sets/Ensembles/Intersection.ind"
 132  cook  = "true"
 133  arity = "2">
 134                 <mapp>
 135                         <mop tag="intersect"/>
 136                         <param id="1" mode="set"/>
 137                         <param id="2" mode="set"/>
 138                 </mapp>
 139 </Operator>
 140
 141 <Operator
 142  name  = "INTERSECTION"
 143  uri   = "cic:/Coq/Sets/Ensembles/Intersection.ind"
 144  cook  = "true"
 145  arity = "3">
 146                 <mapp>
 147                         <m:in/>
 148                         <param id="3"/>
 149                         <m:apply>
 150                                 <mop tag="intersect"/>
 151                                 <param id="1" mode="set"/>
 152                                 <param id="2" mode="set"/>
 153                         </m:apply>
 154                 </mapp>
 155 </Operator>
 156
 157 <Operator
 158  name  = "UNION"
 159  uri   = "cic:/Coq/Sets/Ensembles/Union.ind"
 160  cook  = "true"
 161  arity = "2">
 162                 <mapp>
 163                         <mop tag="union"/>
 164                         <param id="1" mode="set"/>
 165                         <param id="2" mode="set"/>
 166                 </mapp>
 167 </Operator>
 168
 169 <Operator
 170  name  = "UNION"
 171  uri   = "cic:/Coq/Sets/Ensembles/Union.ind"
 172  cook  = "true"
 173  arity = "3">
 174                 <mapp>
 175                         <m:in/>
 176                         <param id="3"/>
 177                         <m:apply>
 178                                 <mop tag="union"/>
 179                                 <param id="1" mode="set"/>
 180                                 <param id="2" mode="set"/>
 181                         </m:apply>
 182                 </mapp>
 183 </Operator>
 184
 185 <Operator
 186  name  = "INCLUDED"
 187  uri   = "cic:/Coq/Sets/Ensembles/Included.con"
 188  cook  = "true"
 189  arity = "2">
 190         <mapp>
 191                 <mop tag="subset"/>
 192                 <param id="1" mode="set"/>
 193                 <param id="2" mode="set"/>
 194         </mapp>
 195 </Operator>
 196
 197 <Operator
 198  name  = "STRICTLY INCLUDED"
 199  uri   = "cic:/Coq/Sets/Ensembles/Strict_Included.con"
 200  cook  = "true"
 201  arity = "2">
 202         <mapp>
 203                 <mop tag="prsubset"/>
 204                 <param id="1" mode="set"/>
 205                 <param id="2" mode="set"/>
 206         </mapp>
 207 </Operator>
 208
 209 <Operator
 210  name  = "SET-DIFF"
 211  uri   = "cic:/Coq/Sets/Ensembles/Setminus.con"
 212  cook  = "true"
 213  arity = "2">
 214                 <mapp>
 215                         <mop tag="setdiff"/>
 216                         <param id="1" mode="set"/>
 217                         <param id="2" mode="set"/>
 218                 </mapp>
 219 </Operator>
 220
 221 <Operator
 222  name  = "SET-DIFF"
 223  uri   = "cic:/Coq/Sets/Ensembles/Setminus.con"
 224  cook  = "true"
 225  arity = "3">
 226                 <mapp>
 227                         <m:in/>
 228                         <param id="3"/>
 229                         <m:apply>
 230                                 <mop tag="setdiff"/>
 231                                 <param id="1" mode="set"/>
 232                                 <param id="2" mode="set"/>
 233                         </m:apply>
 234                 </mapp>
 235 </Operator>
 236
 237 <Operator
 238  name  = "ADD-ELEM"
 239  uri   = "cic:/Coq/Sets/Ensembles/Add.con"
 240  cook  = "true"
 241  arity = "2">
 242                 <mapp>
 243                         <mop tag="union"/>
 244                         <param id="1" mode="set"/>
 245                         <m:set>
 246                                 <param id="2" mode="set"/>
 247                         </m:set>
 248                 </mapp>
 249 </Operator>
 250
 251 <Operator
 252  name  = "ADD-ELEM"
 253  uri   = "cic:/Coq/Sets/Ensembles/Add.con"
 254  cook  = "true"
 255  arity = "3">
 256                 <mapp>
 257                         <m:in/>
 258                         <param id="3"/>
 259                         <m:apply>
 260                                 <mop tag="union"/>
 261                                 <param id="1" mode="set"/>
 262                                 <m:set>
 263                                         <param id="2"/>
 264                                 </m:set>
 265                         </m:apply>
 266                 </mapp>
 267 </Operator>
 268
 269 <Operator
 270  name  = "SUBTRACT-ELEM"
 271  uri   = "cic:/Coq/Sets/Ensembles/Subtract.con"
 272  cook  = "true"
 273  arity = "2">
 274                 <mapp>
 275                         <mop tag="setdiff"/>
 276                         <param id="1" mode="set"/>
 277                         <m:set>
 278                                 <param id="2"/>
 279                         </m:set>
 280                 </mapp>
 281 </Operator>
 282
 283 <Operator
 284  name  = "SUBTRACT-ELEM"
 285  uri   = "cic:/Coq/Sets/Ensembles/Subtract.con"
 286  cook  = "true"
 287  arity = "3">
 288                 <mapp>
 289                         <m:in/>
 290                         <param id="3"/>
 291                         <m:apply>
 292                                 <mop tag="setdiff"/>
 293                                 <param id="1" mode="set"/>
 294                                 <m:set>
 295                                         <param id="2"/>
 296                                 </m:set>
 297                         </m:apply>
 298                 </mapp>
 299 </Operator>
 300
 301 <Operator
 302  name  = "CARD"
 303  uri   = "cic:/Coq/Sets/Finite_sets/cardinal.ind"
 304  cook  = "true"
 305  arity = "2">
 306         <mapp>
 307                 <m:eq/>
 308                 <m:apply>
 309                         <mop tag="card"/>
 310                         <param id="1" mode="set"/>
 311                 </m:apply>
 312                 <param id="2"/>
 313         </mapp>
 314 </Operator>
 315
 316 <Operator
 317  name  = "SIGMA"
 318  uri   = "cic:/Coq/Init/Specif/sig.ind"
 319  arity = "2">
 320         <m:set>
 321                 <mbvar name="x">
 322                         <m:type>
 323                                 <param id="1"/>
 324                         </m:type>
 325                 </mbvar>
 326                 <m:condition>
 327                         <param id="2" bvar="x"/>
 328                 </m:condition>
 329         </m:set>
 330 </Operator>
 331
 332 </OpList>