helm/meta_style/reals.xml

   1 <!DOCTYPE OpList SYSTEM "operator.dtd">
   2
   3 <OpList xmlns:m="http://www.w3.org/1998/Math/MathML">
   4
   5 <!-- Unary Operations and power -->
   6
   7 <Operator
   8  name  = "0"
   9  uri   = "cic:/Coq/Reals/Rdefinitions/R0.con">
  10         <mop tag="cn">0</mop>
  11 </Operator>
  12
  13 <Operator
  14  name  = "1"
  15  uri   = "cic:/Coq/Reals/Rdefinitions/R1.con">
  16         <mop tag="cn">1</mop>
  17 </Operator>
  18
  19 <Operator
  20  name  = "*****"
  21  uri   = "cic:/Coq/Reals/Rdefinitions/Ropp.con"
  22  arity = "1"
  23  m-tag = "minus"/>
  24
  25 <Operator
  26  name  = "*****"
  27  uri   = "cic:/Coq/Reals/Rbasic_fun/Rabsolu.con"
  28  arity = "1"
  29  m-tag = "abs"/>
  30
  31 <Operator
  32  name  = "*****"
  33  uri   = "cic:/Coq/Reals/Rfunctions/fact.con"
  34  arity = "1"
  35  m-tag = "factorial"/>
  36
  37 <Operator
  38  name  = "*****"
  39  uri   = "cic:/Coq/Reals/Rbase/Rsqr.con"
  40  arity = "1">
  41         <mapp>
  42                 <mop tag="power"/>
  43                 <param id="1"/>
  44                 <m:cn>2</m:cn>
  45         </mapp>
  46 </Operator>
  47
  48 <Operator
  49  name  = "*****"
  50  uri   = "cic:/Coq/Reals/Rdefinitions/Rinv.con"
  51  arity = "1">
  52         <mapp>
  53                 <mop tag="power"/>
  54                 <param id="1"/>
  55                 <mapp>
  56                         <mop tag="minus"/>
  57                         <m:cn>1</m:cn>
  58                 </mapp>
  59         </mapp>
  60 </Operator>
  61
  62 <!-- Binary Operations and Relations -->
  63
  64 <Operator
  65  name  = "*****"
  66  uri   = "cic:/Coq/Reals/Rdefinitions/Rle.con"
  67  arity = "2"
  68  m-tag = "leq"/>
  69
  70 <Operator
  71  name  = "*****"
  72  uri   = "cic:/Coq/Reals/Rdefinitions/Rlt.con"
  73  arity = "2"
  74  m-tag = "lt"/>
  75
  76 <Operator
  77  name  = "*****"
  78  uri   = "cic:/Coq/Reals/Rdefinitions/Rge.con"
  79  arity = "2"
  80  m-tag = "geq"/>
  81
  82 <Operator
  83  name  = "*****"
  84  uri   = "cic:/Coq/Reals/Rdefinitions/Rgt.con"
  85  arity = "2"
  86  m-tag = "gt"/>
  87
  88 <Operator
  89  name  = "*****"
  90  uri   = "cic:/Coq/Reals/Rdefinitions/Rplus.con"
  91  arity = "2"
  92  m-tag = "plus"/>
  93
  94 <Operator
  95  name  = "*****"
  96  uri   = "cic:/Coq/Reals/Rdefinitions/Rminus.con"
  97  arity = "2"
  98  m-tag = "minus"/>
  99
 100 <Operator
 101  name  = "*****"
 102  uri   = "cic:/Coq/Reals/Rdefinitions/Rmult.con"
 103  arity = "2"
 104  m-tag = "times"/>
 105
 106 <Operator
 107  name  = "*****"
 108  uri   = "cic:/Coq/Reals/Rdefinitions/Rdiv.con"
 109  arity = "2"
 110  m-tag = "divide"/>
 111
 112 <Operator
 113  name  = "*****"
 114  uri   = "cic:/Coq/Reals/Rbasic_fun/Rmin.con"
 115  arity = "2"
 116  m-tag = "min"/>
 117
 118 <Operator
 119  name  = "*****"
 120  uri   = "cic:/Coq/Reals/Rbasic_fun/Rmax.con"
 121  arity = "2"
 122  m-tag = "max"/>
 123
 124 <Operator
 125  name  = "*****"
 126  uri   = "cic:/Coq/Reals/Rfunctions/pow.con"
 127  arity = "2"
 128  m-tag = "power"/>
 129
 130 <Operator
 131  name  = "LIMIT"
 132  uri   = "cic:/Coq/Reals/Rlimit/limit1_in.con"
 133  arity = "4">
 134         <m:apply>
 135                 <m:eq/>
 136                 <mapp>
 137                         <mop tag="limit"/>
 138                         <mbvar name="x"/>
 139                         <m:lowlimit>
 140                                 <param id="4"/>
 141                         </m:lowlimit>
 142                         <param id="1" bvar="x"/>
 143                 </mapp>
 144                 <param id="3"/>
 145         </m:apply>
 146 </Operator>
 147
 148 <Operator
 149  name  = "DIFFERENTIATION"
 150  uri   = "cic:/Coq/Reals/Rderiv/D_in.con"
 151  arity = "3">
 152         <m:apply>
 153                 <m:eq/>
 154                 <mapp>
 155                         <mop tag="diff"/>
 156                         <mbvar name="x"/>
 157                         <param id="1" bvar="x"/>
 158                 </mapp>
 159                 <param id="3"/>
 160         </m:apply>
 161 </Operator>
 162
 163 </OpList>