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