]> matita.cs.unibo.it Git - helm.git/commitdiff
projects / helm.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 8ad6f45)
improved input syntax page with example queries of elim, match and hint
authorStefano Zacchiroli <zack@upsilon.cc>
Tue, 21 Dec 2004 17:48:59 +0000 (17:48 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Tue, 21 Dec 2004 17:48:59 +0000 (17:48 +0000)
helm/searchEngine/html/moogle_syntax.html patch | blob | history

diff --git a/helm/searchEngine/html/moogle_syntax.html b/helm/searchEngine/html/moogle_syntax.html
index 80e45ca199388b0456054ad03d8b751e1fbf7f5f..2d783940986ffbe95e3b9b007039a0e435297db4 100644 (file)
--- a/helm/searchEngine/html/moogle_syntax.html
+++ b/helm/searchEngine/html/moogle_syntax.html
@@ -3,6 +3,8 @@
     <style type="text/css">
       ul.spaced li { padding-bottom: 1em; }
       ul.empty li { list-style-type: none; }
+      tt { font-weight: bold; background-color: lightgray; }
+      tt.uri { font-weight: normal; background-color: transparent; }
     </style>
   </head>
   <body>
@@ -27,27 +29,66 @@
            <u>Examples:</u>
            <ul class="empty">
              <li> <tt>nat</tt> pattern matches
-             <tt>cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)</tt> only
+             <tt class="uri">cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)</tt> only
              </li>
              <li> <tt>n?t</tt> pattern matches
-             <tt>cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)</tt> and
-             <tt>cic:/Coq/Init/Logic/not.con</tt>
+             <tt class="uri">cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)</tt> and
+             <tt class="uri">cic:/Coq/Init/Logic/not.con</tt>
              </li>
              <li> <tt>nat*</tt> pattern matches
-             <tt>cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)</tt>,
-             <tt>cic:/Coq/Init/Peano/nat_case.con</tt> and many more
+             <tt class="uri">cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)</tt>,
+             <tt class="uri">cic:/Coq/Init/Peano/nat_case.con</tt> and many more
              </li>
            </ul>
            </p>
            </li>
            <li>
-           <b>hint</b>
+           <b>match <em>&lt;term&gt;</em></b>
+           <p>
+           <u>Examples:</u>
+           <ul class="empty">
+             <li> <tt>\forall x,y:nat.x+y=y+x</tt>
+             (commutativity of natural plus)
+             </li>
+             <li> <tt>\forall x,y,z:R.x*(y+z)=x*y+x*z</tt>
+             (distributivity of real times over real plus)
+             </li>
+             <li> <tt>nat \to nat \to nat</tt>
+             (all binary functions over naturals)
+             </li>
+           </ul>
+           </p>
            </li>
            <li>
-           <b>match</b>
+           <b>hint <em>&lt;term&gt;</em></b>
+           <p>
+           <u>Examples:</u>
+           <ul class="empty">
+             <li> <tt>\forall n:nat. (fact n) = n * (fact (n - 1))</tt>
+             (how could we prove <em>n! = (n-1)! * n</em> ?)
+             </li>
+             <li> <tt>\forall n:nat.n \lt n+5</tt>
+             (how could we prove <em>n &lt; n + 5</em> ?)
+             </li>
+             <li> <tt>\forall x,y:nat. x*y \lt (S x)*(S y)</tt>
+             (how could we prove <em>x*y &lt; (x+1)*(y+1)</em> ?)
+             </li>
+           </ul>
+           </p>
            </li>
            <li>
-           <b>elim</b>
+           <b>elim <em>&lt;identifier&gt;</em></b>
+           <p>
+           <u>Examples:</u>
+           <ul class="empty">
+             <li> <tt>nat</tt>
+             (induction/elimination principles over natural numbers)
+             </li>
+             <li> <tt>list</tt>
+             (induction/elimination principles over lists)
+             </li>
+           </ul>
+           </p>
            </li>
          </ul>
        </td>
Unnamed repository; edit this file 'description' to name the repository.