X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FsearchEngine%2Fhtml%2Fgrammarpdq.html;h=bd3835bf90eeb3005ec6ad7d4264a78b447f62dd;hb=fb783535ecfe90b6277605d8c8df395389acaf75;hp=55fec767328516ab221cbb33863de1328a984015;hpb=fb12bdf2cf0ecbf50726b70d6a3097cb933319a0;p=helm.git diff --git a/helm/searchEngine/html/grammarpdq.html b/helm/searchEngine/html/grammarpdq.html index 55fec7673..bd3835bf9 100644 --- a/helm/searchEngine/html/grammarpdq.html +++ b/helm/searchEngine/html/grammarpdq.html @@ -5,18 +5,34 @@
-<Id>::=[ 'A-Z' | 'a-z' ][ 'A-Z' | 'a-z' | '0-9' | \- | _ | \' ]*
+<Id>::= [ 'A-Z' | 'a-z' ][ 'A-Z' | 'a-z' | '0-9' | \- | _ | \' ]* - +
<Uri>::= <Conuri> | <Varuri> | <Indtyuri> | <Indconuri> - +
<Conuri>::= "cic:/" [<Id> "/" ]*<Id> ".con" - +
<Varuri>::= "cic:/" [<Id> "/" ]*<Id> ".var" - +
<Indtyuri>::= "cic:/" [<Id> "/" ]*<Id> ".ind#1/" ['0-9']+
- <Indconuri>::="cic:/" [<Id> "/" ]*<Id> ".ind#1/" ['0-9']+ "/" ['0-9']+
<Indconuri>::= "cic:/" [<Id> "/" ]*<Id> ".ind#1/" ['0-9']+ "/" ['0-9']+
- <Exp_Named_Subst>::="{" [ [ [<Id> | <Varuri> ] ":=" <Expression> ";" ]* [ [<Id> | <Varuri> ] ":=" <Expression> ] ]? "}"
<Exp_Named_Subst>::= "{" [ [ [<Id> | <Varuri> ] ":=" <Expression> ";" ]* [ [<Id> | <Varuri> ] ":=" <Expression> ] ]? "}"
+
+ <Alias>::= "alias" <Id> <Uri>
+
+ <Genid>::= [ <Id> | <Varuri> | <Indtyuri> | <Indconuri> ] <Exp_Named_Subst>
+
+ <Expr>::= "\" <Genid> [ ":" | ":=" ] <Expr>"."<Expr>
+
+::= "!" <Genid> ":" <Expr>"."<Expr>
+
+::= <Expr>"->"<Expr>
+
+::= "(" <Expr> ")" "->"<Expr>
+
+::= "(" <Expr> [ " " <Expr>]* ")"
+
+::= "Prop" | "Set" | "Type" | "?" | <Uri> | <Id>