From 08fc8d34cc017b75eafcaec7bd314c8f49d6e320 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 3 Dec 2004 16:05:27 +0000 Subject: [PATCH] moogle syntax help page, actually contains only syntax and examples for the "locate" query. "hint", "match" and "elim" syntaxes are currently undocumented --- helm/searchEngine/html/moogle_syntax.html | 57 +++++++++++++++++++++++ 1 file changed, 57 insertions(+) create mode 100644 helm/searchEngine/html/moogle_syntax.html 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 +
    • +
+
+ + -- 2.39.2