helm/meta_style/basic.xml

   1 <!DOCTYPE OpList SYSTEM "operator.dtd">
   2
   3
   4 <OpList xmlns:m="http://www.w3.org/1998/Math/MathML">
   5
   6 <!-- ************************* LOGIC *********************************-->
   7
   8 <Operator
   9  name  = "AND"
  10  uri   = "cic:/Coq/Init/Logic/and.ind"
  11  arity = "2"
  12  m-tag = "and"/>
  13
  14 <Operator
  15  name  = "OR"
  16  uri   = "cic:/Coq/Init/Logic/or.ind"
  17  arity = "2"
  18  m-tag = "or"/>
  19
  20 <Operator
  21  name  = "IFF"
  22  uri   = "cic:/Coq/Init/Logic/iff.con"
  23  arity = "2">
  24         <mapp>
  25                 <m:csymbol>iff</m:csymbol>
  26                 <param id="1"/>
  27                 <param id="2"/>
  28         </mapp>
  29 </Operator>
  30
  31 <Operator
  32  name  = "NOT"
  33  uri   = "cic:/Coq/Init/Logic/not.con"
  34  arity = "1"
  35  m-tag = "not"/>
  36
  37
  38 <!-- EQUALITY and TYPE EQUALITY -->
  39
  40 <Operator
  41  name  = "EQUALITY and TYPE EQUALITY"
  42  uri   = "cic:/Coq/Init/Logic/eq.ind | cic:/Coq/Init/Logic_Type/eqT.ind"
  43  hide  = "1"
  44  arity = "2"
  45  m-tag = "eq"/>
  46
  47 <NotOperator
  48  name  = "NOT-EQ and NOT-EQT"
  49  uri   = "cic:/Coq/Init/Logic/eq.ind | cic:/Coq/Init/Logic_Type/eqT.ind"
  50  hide  = "1"
  51  arity = "2">
  52         <mapp>
  53                 <m:neq/>
  54                 <param id="1"/>
  55                 <param id="2" mode="set"/>
  56         </mapp>
  57 </NotOperator>
  58
  59 <Operator
  60  name  = "EXIST"
  61  uri   = "cic:/Coq/Init/Logic/ex.ind | cic:/Coq/Init/Logic_Type/exT.ind"
  62  arity = "2">
  63         <mapp>
  64                 <mop tag="exists"/>
  65                 <mbvar name="x"/>
  66                 <m:condition>
  67                         <param id="1" mode="pure"/>
  68                 </m:condition>
  69                 <param id="2" bvar="x"/>
  70         </mapp>
  71 </Operator>
  72
  73 <Operator
  74  name  = "EXIST"
  75  uri   = "cic:/Coq/Init/Logic/ex2.ind | cic:/Coq/Init/Logic_Type/exT2.ind"
  76  hide  = "1"
  77  arity = "2">
  78         <mapp>
  79                 <mop tag="exists"/>
  80                 <mbvar name="x"/>
  81                 <m:condition>
  82                         <param id="1" bvar="x"/>
  83                 </m:condition>
  84                 <param id="2" bvar="x"/>
  85         </mapp>
  86 </Operator>
  87
  88 </OpList>