helm/meta_style/set.xml

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