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 <import href="positive.xsl"/>
   8
   9 <!-- CSC: manca
  10 <Operator
  11  name  = "CONS"
  12  uri   = "cic:/Coq/Lists/PolyList/list.ind"
  13  arity = "2"
  14  m-tag = "???"/>
  15
  16 <Operator
  17  name  = "NIL"
  18  uri   = "cic:/Coq/Lists/PolyList/list.ind"
  19  arity = "0"
  20  m-tag = "???"/> -->
  21
  22 <Operator
  23  name  = "APPEND"
  24  uri   = "cic:/Coq/Lists/PolyList/app.con"
  25  cook  = "true"
  26  arity = "2">
  27         <mapp>
  28                 <m:csymbol>append</m:csymbol>
  29                 <param id="1"/>
  30                 <param id="2"/>
  31         </mapp>
  32 </Operator>
  33
  34 <Operator
  35  name  = "IN"
  36  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"
  37  cook  = "true"
  38  arity = "2"
  39  m-tag = "in"/>
  40
  41 <Operator
  42  name  = "INCL"
  43  uri   = "cic:/Coq/Lists/PolyList/incl.con"
  44  cook  = "true"
  45  arity = "2"
  46  m-tag = "subset"/>
  47
  48 <Operator
  49  name  = "INTER"
  50  uri   = "cic:/Coq/Lists/ListSet/set_inter.con"
  51  cook  = "true"
  52  arity = "2"
  53  m-tag = "intersect"/>
  54
  55 <Operator
  56  name  = "LENGTH"
  57  uri   = "cic:/Coq/Lists/PolyList/length.con"
  58  cook  = "true"
  59  arity = "1"
  60  m-tag = "card"/>
  61
  62 </OpList>