From: Stefano Zacchiroli Date: Fri, 3 Dec 2004 16:05:27 +0000 (+0000) Subject: moogle syntax help page, actually contains only syntax and examples for X-Git-Tag: V_0_1_0~169 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=08fc8d34cc017b75eafcaec7bd314c8f49d6e320;p=helm.git moogle syntax help page, actually contains only syntax and examples for the "locate" query. "hint", "match" and "elim" syntaxes are currently undocumented --- diff --git a/helm/searchEngine/html/moogle_syntax.html b/helm/searchEngine/html/moogle_syntax.html new file mode 100644 index 000000000..80e45ca19 --- /dev/null +++ b/helm/searchEngine/html/moogle_syntax.html @@ -0,0 +1,57 @@ + + + + + + + + + + + + +
+ moogle +
+

Moogle Input Syntax

+
    +
  • + locate <pattern> +

    + <pattern> is a shell like pattern which could + include * (denoting any sequence of 0 or more characters) + and ? (denoting any single character).
    +

    +

    + Examples: +

      +
    • nat pattern matches + cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1) only +
      • +
    • n?t pattern matches + cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1) and + cic:/Coq/Init/Logic/not.con +
      • +
    • nat* pattern matches + cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1), + cic:/Coq/Init/Peano/nat_case.con and many more +
      • +
    +

    +
    • +
  • + hint +
    • +
  • + match +
    • +
  • + elim +
    • +
+
+ +