X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FsearchEngine%2Fhtml%2Fmoogle_syntax.html;h=7fa0fe380b459b552c393988efbd9325328d4fd5;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=80e45ca199388b0456054ad03d8b751e1fbf7f5f;hpb=08fc8d34cc017b75eafcaec7bd314c8f49d6e320;p=helm.git diff --git a/helm/searchEngine/html/moogle_syntax.html b/helm/searchEngine/html/moogle_syntax.html index 80e45ca19..7fa0fe380 100644 --- a/helm/searchEngine/html/moogle_syntax.html +++ b/helm/searchEngine/html/moogle_syntax.html @@ -3,18 +3,20 @@
- moogle + whelp
-

Moogle Input Syntax

+

Whelp Input Syntax

  • locate <pattern> @@ -27,27 +29,66 @@ Examples:
    • nat pattern matches - cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1) only + 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 + 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 + cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1), + cic:/Coq/Init/Peano/nat_case.con and many more

  • - hint + match <term> +

    + Examples: +

      +
    • \forall x,y:nat.x+y=y+x + (commutativity of natural plus) +
      • +
    • \forall x,y,z:R.x*(y+z)=x*y+x*z + (distributivity of real times over real plus) +
      • +
    • nat \to nat \to nat + (all binary functions over naturals) +
      • +
    +

  • - match + hint <term> +

    + Examples: +

      +
    • \forall n:nat. (fact n) = n * (fact (n - 1)) + (how could we prove n! = (n-1)! * n ?) +
      • +
    • \forall n:nat.n \lt n+5 + (how could we prove n < n + 5 ?) +
      • +
    • \forall x,y:nat. x*y \lt (S x)*(S y) + (how could we prove x*y < (x+1)*(y+1) ?) +
      • +
    +

  • - elim + elim <identifier> +

    + Examples: +

      +
    • nat + (induction/elimination principles over natural numbers) +
      • +
    • list + (induction/elimination principles over lists) +
      • +
    +