helm/searchEngine/html/moogle_syntax.html

   1 <html>
   2   <head>
   3     <style type="text/css">
   4       ul.spaced li { padding-bottom: 1em; }
   5       ul.empty li { list-style-type: none; }
   6       tt { font-weight: bold; background-color: lightgray; }
   7       tt.uri { font-weight: normal; background-color: transparent; }
   8     </style>
   9   </head>
  10   <body>
  11     <table>
  12       <tr>
  13         <td>
  14           <img align="center" src="http://helm.cs.unibo.it/whelp.png" alt="whelp" />
  15         </td>
  16       </tr>
  17       <tr>
  18         <td>
  19           <h2>Whelp Input Syntax</h2>
  20           <ul class="spaced">
  21             <li>
  22             <b>locate <em>&lt;pattern&gt;</em></b>
  23             <p>
  24             <em>&lt;pattern&gt;</em> is a shell like pattern which could
  25             include <tt>*</tt> (denoting any sequence of 0 or more characters)
  26             and <tt>?</tt> (denoting any single character).<br />
  27             </p>
  28             <p>
  29             <u>Examples:</u>
  30             <ul class="empty">
  31               <li> <tt>nat</tt> pattern matches
  32               <tt class="uri">cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)</tt> only
  33               </li>
  34               <li> <tt>n?t</tt> pattern matches
  35               <tt class="uri">cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)</tt> and
  36               <tt class="uri">cic:/Coq/Init/Logic/not.con</tt>
  37               </li>
  38               <li> <tt>nat*</tt> pattern matches
  39               <tt class="uri">cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)</tt>,
  40               <tt class="uri">cic:/Coq/Init/Peano/nat_case.con</tt> and many more
  41               </li>
  42             </ul>
  43             </p>
  44             </li>
  45             <li>
  46             <b>match <em>&lt;term&gt;</em></b>
  47             <p>
  48             <u>Examples:</u>
  49             <ul class="empty">
  50               <li> <tt>\forall x,y:nat.x+y=y+x</tt>
  51               (commutativity of natural plus)
  52               </li>
  53               <li> <tt>\forall x,y,z:R.x*(y+z)=x*y+x*z</tt>
  54               (distributivity of real times over real plus)
  55               </li>
  56               <li> <tt>nat \to nat \to nat</tt>
  57               (all binary functions over naturals)
  58               </li>
  59             </ul>
  60             </p>
  61             </li>
  62             <li>
  63             <b>hint <em>&lt;term&gt;</em></b>
  64             <p>
  65             <u>Examples:</u>
  66             <ul class="empty">
  67               <li> <tt>\forall n:nat. (fact n) = n * (fact (n - 1))</tt>
  68               (how could we prove <em>n! = (n-1)! * n</em> ?)
  69               </li>
  70               <li> <tt>\forall n:nat.n \lt n+5</tt>
  71               (how could we prove <em>n &lt; n + 5</em> ?)
  72               </li>
  73               <li> <tt>\forall x,y:nat. x*y \lt (S x)*(S y)</tt>
  74               (how could we prove <em>x*y &lt; (x+1)*(y+1)</em> ?)
  75               </li>
  76             </ul>
  77             </p>
  78             </li>
  79             <li>
  80             <b>elim <em>&lt;identifier&gt;</em></b>
  81             <p>
  82             <u>Examples:</u>
  83             <ul class="empty">
  84               <li> <tt>nat</tt>
  85               (induction/elimination principles over natural numbers)
  86               </li>
  87               <li> <tt>list</tt>
  88               (induction/elimination principles over lists)
  89               </li>
  90             </ul>
  91             </p>
  92             </li>
  93           </ul>
  94         </td>
  95       </tr>
  96     </table>
  97   </body>
  98 </html>