X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2FsearchEngine%2Fhtml%2Fmoogle_syntax.html;h=2d783940986ffbe95e3b9b007039a0e435297db4;hb=eac74259f5a0aaa8056791876284c897a6827c24;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..2d7839409 100644
--- a/helm/searchEngine/html/moogle_syntax.html
+++ b/helm/searchEngine/html/moogle_syntax.html
@@ -3,6 +3,8 @@
@@ -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)
+
+
+