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