helm/meta_style/list.xml

   1 <!DOCTYPE OpList SYSTEM "operator.dtd">
   2
   3 <!-- ************************** LISTS ****************************** -->
   4
   5 <OpList xmlns:m="http://www.w3.org/1998/Math/MathML">
   6
   7 <!-- CSC: manca
   8 <Operator
   9  name  = "CONS"
  10  uri   = "cic:/Coq/Lists/PolyList/list.ind"
  11  arity = "2"
  12  m-tag = "???"/>
  13
  14 <Operator
  15  name  = "NIL"
  16  uri   = "cic:/Coq/Lists/PolyList/list.ind"
  17  arity = "0"
  18  m-tag = "???"/> -->
  19
  20 <Operator
  21  name  = "APPEND"
  22  uri   = "cic:/Coq/Lists/PolyList/app.con"
  23  cook  = "true"
  24  arity = "2">
  25         <mapp>
  26                 <m:csymbol>append</m:csymbol>
  27                 <param id="1"/>
  28                 <param id="2"/>
  29         </mapp>
  30 </Operator>
  31
  32 <Operator
  33  name  = "IN"
  34  uri   = "cic:/Coq/Lists/PolyList/In.con | cic:/Coq/Lists/TheoryList/In_spec.ind | cic:/Coq/Lists/ListSet/set_In.con | cic:/Coq/Lists/ListSet/set_mem.con"
  35  cook  = "true"
  36  arity = "2"
  37  m-tag = "in"/>
  38
  39 <Operator
  40  name  = "INCL"
  41  uri   = "cic:/Coq/Lists/PolyList/incl.con"
  42  cook  = "true"
  43  arity = "2"
  44  m-tag = "subset"/>
  45
  46 <Operator
  47  name  = "INTER"
  48  uri   = "cic:/Coq/Lists/ListSet/set_inter.con"
  49  cook  = "true"
  50  arity = "2"
  51  m-tag = "intersect"/>
  52
  53 <Operator
  54  name  = "LENGTH"
  55  uri   = "cic:/Coq/Lists/PolyList/length.con"
  56  cook  = "true"
  57  arity = "1"
  58  m-tag = "card"/>
  59
  60 </OpList>