From 80dac1feac6f058f6beb0a5ffbddf3a5139fa336 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 21 Dec 2004 17:48:59 +0000 Subject: [PATCH] improved input syntax page with example queries of elim, match and hint --- helm/searchEngine/html/moogle_syntax.html | 57 +++++++++++++++++++---- 1 file changed, 49 insertions(+), 8 deletions(-) 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) +

-- 2.39.2