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