From: Stefano Zacchiroli Date: Tue, 21 Dec 2004 17:48:59 +0000 (+0000) Subject: improved input syntax page with example queries of elim, match and hint X-Git-Tag: V_0_1_0~156 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=80dac1feac6f058f6beb0a5ffbddf3a5139fa336;p=helm.git improved input syntax page with example queries of elim, match and hint --- 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) +