helm/meta_style/arith.xml

   1 <!DOCTYPE OpList SYSTEM "operator.dtd">
   2
   3 <!-- ************************** ARITHMETICS ****************************** -->
   4
   5 <OpList xmlns:m="http://www.w3.org/1998/Math/MathML">
   6
   7 <Operator
   8  name  = "LESS EQUAL"
   9  uri   = "cic:/Coq/Init/Peano/le.ind | cic:/Coq/ZArith/zarith_aux/Zle.con"
  10  arity = "2"
  11  m-tag = "leq"/>
  12
  13 <Operator
  14  name  = "LESS THAN"
  15  uri   = "cic:/Coq/Init/Peano/lt.con | cic:/Coq/ZArith/zarith_aux/Zlt.con"
  16  arity = "2"
  17  m-tag = "lt"/>
  18
  19 <Operator
  20  name  = "GREATER EQUAL"
  21  uri   = "cic:/Coq/Init/Peano/ge.con | cic:/Coq/ZArith/zarith_aux/Zge.con"
  22  arity = "2"
  23  m-tag = "geq"/>
  24
  25 <Operator
  26  name  = "GREATER THAN"
  27  uri   = "cic:/Coq/Init/Peano/gt.con | cic:/Coq/ZArith/zarith_aux/Zgt.con"
  28  arity = "2"
  29  m-tag = "gt"/>
  30
  31 <Operator
  32  name  = "*****"
  33  uri   = "cic:/Coq/Init/Peano/plus.con | cic:/Coq/ZArith/fast_integer/Zplus.con"
  34  arity = "2"
  35  m-tag = "plus"/>
  36
  37 <Operator
  38  name  = "*****"
  39  uri   = "cic:/Coq/Arith/Minus/minus.con | cic:/Coq/ZArith/zarith_aux/Zminus.con"
  40  arity = "2"
  41  m-tag = "minus"/>
  42
  43 <Operator
  44  name  = "*****"
  45  uri   = "cic:/Coq/Init/Peano/mult.con | cic:/Coq/ZArith/fast_integer/Zmult.con"
  46  arity = "2"
  47  m-tag = "times"/>
  48
  49 <Operator
  50  name  = "*****"
  51  uri   = "cic:/Coq/Arith/Min/min.con | cic:/Coq/ZArith/zarith_aux/Zmin.con"
  52  arity = "2"
  53  m-tag = "min"/>
  54
  55 <Operator
  56  name  = "*****"
  57  uri   = "cic:/Coq/ZArith/fast_integer/Zopp.con"
  58  arity = "1"
  59  m-tag = "minus"/>
  60
  61 <Operator
  62  name  = "*****"
  63  uri   = "cic:/Coq/ZArith/zarith_aux/absolu.con"
  64  arity = "1"
  65  m-tag = "abs"/>
  66
  67 </OpList>