]> matita.cs.unibo.it Git - helm.git/blob - helm/searchEngine/html/grammarpdq.html
Added new function compare_metasenvs.
[helm.git] / helm / searchEngine / html / grammarpdq.html
1 <HTML>
2 <HEAD>
3 <SCRIPT language="Javascript">
4 </SCRIPT>
5 </HEAD>
6 <BODY>
7 <a name="Id">
8 <p><b>&lt;Id&gt;</b>::= [ 'A-Z' | 'a-z' ][ 'A-Z' | 'a-z' | '0-9' | \- | _ | \' ]*</a>
9 <a name="Uri">
10 <p><b>&lt;Uri&gt;</b>::= &lt;<a href="#Conuri">Conuri</a>&gt; | &lt;<a href="#Varuri">Varuri</a>&gt; | &lt;<a href="#Indtyuri">Indtyuri</a>&gt; | &lt;<a href="#Indconuri">Indconuri</a>&gt;</a>
11 <a name="Conuri">
12 <p><b>&lt;Conuri&gt;</b>::= &quot;cic:/&quot; [&lt;<a href="#Id">Id</a>&gt; &quot;/&quot; ]*&lt;<a href="#Id">Id</a>&gt; &quot;.con&quot;</a>
13 <a name="Varuri">
14 <p><b>&lt;Varuri&gt;</b>::= &quot;cic:/&quot; [&lt;<a href="#Id">Id</a>&gt; &quot;/&quot; ]*&lt;<a href="#Id">Id</a>&gt; &quot;.var&quot;</a>
15 <a name="Indtyuri">
16 <p><b>&lt;Indtyuri&gt;</b>::= &quot;cic:/&quot; [&lt;<a href="#Id">Id</a>&gt; &quot;/&quot; ]*&lt;<a href="#Id">Id</a>&gt; &quot;.ind#1/&quot; ['0-9']+</a>
17 <a name="Indconuri">
18 <p><b>&lt;Indconuri&gt;</b>::= &quot;cic:/&quot; [&lt;<a href="#Id">Id</a>&gt; &quot;/&quot; ]*&lt;<a href="#Id">Id</a>&gt; &quot;.ind#1/&quot; ['0-9']+ &quot;/&quot; ['0-9']+</a>
19 <a name="Exp_Named_Subst">
20 <p><b>&lt;Exp_Named_Subst&gt;</b>::= &quot;{&quot; [ [ [&lt;<a href="#Id">Id</a>&gt; | &lt;<a href="#Varuri">Varuri</a>&gt; ] &quot;:=&quot; &lt;Expression&gt; &quot;;&quot; ]* [ [&lt;<a href="#Id">Id</a>&gt; | &lt;<a href="#Varuri">Varuri</a>&gt; ] &quot;:=&quot; &lt;Expression&gt; ] ]? &quot;}&quot;</a>
21 <a name="Alias">
22 <p><b>&lt;Alias&gt;</b>::= &quot;alias&quot; &quot;id&quot; &lt;<a href="#Id">Id</a>&gt; = &lt;<a href="#Uri">Uri</a>&gt;
23 <a name="Genid">
24 <p><b>&lt;Genid&gt;</b>::= [ &lt;<a href="#Id">Id</a>&gt; | &lt;<a href="#Varuri">Varuri</a>&gt; | &lt;<a href="#Indtyuri">Indtyuri</a>&gt; | &lt;<a href="#Indconuri">Indconuri</a>&gt; ] &lt;<a href="#Exp_Named_Subst">Exp_Named_Subst</a>&gt;
25 <a name="Expr">
26 <p><b>&lt;Expr&gt;</b>::= &quot;\&quot; &lt;<a href="#Genid">Genid</a>&gt; [ &quot;:&quot; | &quot;:=&quot; ] &lt;<a href="#Expr">Expr</a>&gt;&quot;.&quot;&lt;<a href="#Expr">Expr</a>&gt;
27 <br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
28 ::= &quot;!&quot; &lt;<a href="#Genid">Genid</a>&gt; &quot;:&quot; &lt;<a href="#Expr">Expr</a>&gt;&quot;.&quot;&lt;<a href="#Expr">Expr</a>&gt;
29 <br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
30 ::= &lt;<a href="#Expr">Expr</a>&gt;&quot;->&quot;&lt;<a href="#Expr">Expr</a>&gt;
31 <br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
32 ::= &quot;(&quot; &lt;<a href="#Expr">Expr</a>&gt; &quot;)&quot; &quot;->&quot;&lt;<a href="#Expr">Expr</a>&gt;
33 <br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
34 ::= &quot;(&quot; &lt;<a href="#Expr">Expr</a>&gt; [ &quot; &quot; &lt;<a href="#Expr">Expr</a>&gt;]* &quot;)&quot;
35 <br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
36 ::= &quot;Prop&quot; | &quot;Set&quot; | &quot;Type&quot; | &quot;?&quot; | &lt;<a href="#Uri">Uri</a>&gt; | &lt;<a href="#Id">Id</a>&gt;
37 </BODY>
38 </HTML>