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     </style>
   7   </head>
   8   <body>
   9     <table>
  10       <tr>
  11         <td>
  12           <img align="center" src="http://helm.cs.unibo.it/moogle.png" alt="moogle" />
  13         </td>
  14       </tr>
  15       <tr>
  16         <td>
  17           <h2>Moogle Input Syntax</h2>
  18           <ul class="spaced">
  19             <li>
  20             <b>locate <em>&lt;pattern&gt;</em></b>
  21             <p>
  22             <em>&lt;pattern&gt;</em> is a shell like pattern which could
  23             include <tt>*</tt> (denoting any sequence of 0 or more characters)
  24             and <tt>?</tt> (denoting any single character).<br />
  25             </p>
  26             <p>
  27             <u>Examples:</u>
  28             <ul class="empty">
  29               <li> <tt>nat</tt> pattern matches
  30               <tt>cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)</tt> only
  31               </li>
  32               <li> <tt>n?t</tt> pattern matches
  33               <tt>cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)</tt> and
  34               <tt>cic:/Coq/Init/Logic/not.con</tt>
  35               </li>
  36               <li> <tt>nat*</tt> pattern matches
  37               <tt>cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)</tt>,
  38               <tt>cic:/Coq/Init/Peano/nat_case.con</tt> and many more
  39               </li>
  40             </ul>
  41             </p>
  42             </li>
  43             <li>
  44             <b>hint</b>
  45             </li>
  46             <li>
  47             <b>match</b>
  48             </li>
  49             <li>
  50             <b>elim</b>
  51             </li>
  52           </ul>
  53         </td>
  54       </tr>
  55     </table>
  56   </body>
  57 </html>