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/Conjunction/and.ind"
  11  arity = "2"
  12  m-tag = "and"/>
  13
  14 <Operator
  15  name  = "OR"
  16  uri   = "cic:/Coq/Init/Logic/Disjunction/or.ind"
  17  arity = "2"
  18  m-tag = "or"/>
  19
  20 <Operator
  21  name  = "NOT"
  22  uri   = "cic:/Coq/Init/Logic/not.con"
  23  arity = "1"
  24  m-tag = "not"/>
  25
  26
  27 <!-- EQUALITY and TYPE EQUALITY -->
  28
  29 <Operator
  30  name  = "EQUALITY and TYPE EQUALITY"
  31  uri   = "cic:/Coq/Init/Logic/Equality/eq.ind | cic:/Coq/Init/Logic_Type/eqT.ind"
  32  hide  = "1"
  33  arity = "2"
  34  m-tag = "eq"/>
  35
  36 <NotOperator
  37  name  = "NOT-EQ and NOT-EQT"
  38  uri   = "cic:/Coq/Init/Logic/Equality/eq.ind | cic:/Coq/Init/Logic_Type/eqT.ind"
  39  hide  = "1"
  40  arity = "2">
  41         <mapp>
  42                 <m:neq/>
  43                 <param id="1"/>
  44                 <param id="2" mode="set"/>
  45         </mapp>
  46 </NotOperator>
  47
  48 <Operator
  49  name  = "EXIST"
  50  uri   = "cic:/Coq/Init/Logic/First_order_quantifiers/ex.ind | cic:/Coq/Init/Logic_Type/exT.ind"
  51  arity = "2">
  52         <mapp>
  53                 <mop tag="exists"/>
  54                 <mbvar name="x"/>
  55                 <m:condition>
  56                         <param id="1" mode="pure"/>
  57                 </m:condition>
  58                 <param id="2" bvar="x"/>
  59         </mapp>
  60 </Operator>
  61
  62 <Operator
  63  name  = "EXIST"
  64  uri   = "cic:/Coq/Init/Logic/First_order_quantifiers/ex2.ind | cic:/Coq/Init/Logic_Type/exT2.ind"
  65  hide  = "1"
  66  arity = "2">
  67         <mapp>
  68                 <mop tag="exists"/>
  69                 <mbvar name="x"/>
  70                 <m:condition>
  71                         <param id="1" bvar="x"/>
  72                 </m:condition>
  73                 <param id="2" bvar="x"/>
  74         </mapp>
  75 </Operator>
  76
  77 </OpList>