]> matita.cs.unibo.it Git - helm.git/commitdiff
projects / helm.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: a3ab07c)
basic_1: we separate theorems and lemmas as in basic_2
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 20 Jan 2015 17:51:37 +0000 (17:51 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 20 Jan 2015 17:51:37 +0000 (17:51 +0000)
         the informational page is complete

helm/www/lambdadelta/BTM.html patch | blob | history
helm/www/lambdadelta/apps_2.html patch | blob | history
helm/www/lambdadelta/basic_1.html patch | blob | history
helm/www/lambdadelta/basic_2.html patch | blob | history
helm/www/lambdadelta/documentation.html patch | blob | history
helm/www/lambdadelta/download/lambdadelta_1.tar.gz patch | blob | history
helm/www/lambdadelta/ground_2.html patch | blob | history
helm/www/lambdadelta/implementation.html patch | blob | history
helm/www/lambdadelta/index.html patch | blob | history
helm/www/lambdadelta/news.html patch | blob | history
helm/www/lambdadelta/specification.html patch | blob | history

diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html
index 0b76467b10f98290f0cde0db814485291b5a39f3..8cda8f76abfe9f1e610dce6e362d32d7cc5ad42b 100644 (file)
--- a/helm/www/lambdadelta/BTM.html
+++ b/helm/www/lambdadelta/BTM.html
@@ -222,6 +222,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Mon, 19 Jan 2015 23:52:51 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 20 Jan 2015 18:39:00 +0100</div>
   </body>
 </html>
diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html
index 75a2a5a055323809bd669919575d9c9a197500f9..7938d47dacd09e87a1e22eeb2c689df6fe877faf 100644 (file)
--- a/helm/www/lambdadelta/apps_2.html
+++ b/helm/www/lambdadelta/apps_2.html
@@ -258,6 +258,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Mon, 19 Jan 2015 23:52:52 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 20 Jan 2015 18:39:00 +0100</div>
   </body>
 </html>
diff --git a/helm/www/lambdadelta/basic_1.html b/helm/www/lambdadelta/basic_1.html
index 0b8626498731c56ab9eae528ecdefbebefad802f..4871fb70f9c39dcc2074601fc5491ed4a0897a2c 100644 (file)
--- a/helm/www/lambdadelta/basic_1.html
+++ b/helm/www/lambdadelta/basic_1.html
@@ -102,18 +102,68 @@
         </tbody>
       </table>
     </div>
-    <!--   
-   <section>System's Syntax and Behavior</section>
-   <body>This is a summary of the "block structure"
-         of the System's syntactic items and reductions.
-   </body>
-   <table name="basic_1_blk"/>
-   <body>* In terms only.
-         ** In terms and local environments only.
-         *** In global environments only.
-         **** Sort level k in terms only.
-   </body>
--->
+    <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="">Abstract Syntax and Behavior <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b6.png" />
+    </div>
+    <div xmlns:ld="http://lambdadelta.info/" class="text">This is a summary of available syntactic items and reductions (block structure).
+   </div>
+    <div xmlns:ld="http://lambdadelta.info/" class="text">
+      <table cellpadding="4" cellspacing="0">
+        <tbody>
+          <tr>
+            <td class="snns top gray">domain</td>
+            <td class="snns top italic gray">block</td>
+            <td class="snns top gray">leader</td>
+            <td class="snns top gray">→ζ *</td>
+            <td class="snns top gray">annotator (with →ϵ *)</td>
+            <td class="snns top gray">applicator (with →θ *)</td>
+            <td class="snns top gray">reference *</td>
+            <td class="ssns top gray">reduction</td>
+          </tr>
+          <tr>
+            <td class="snns top">{X | Γ ⊢ ⊤}</td>
+            <td class="snns top italic wine">exclusion</td>
+            <td class="snns top wine">Γ ⊢ χ</td>
+            <td class="snns top wine">yes</td>
+            <td class="snns top wine">no</td>
+            <td class="snns top wine">no</td>
+            <td class="snns top wine">no</td>
+            <td class="ssns top wine">no</td>
+          </tr>
+          <tr>
+            <td class="snns top">{X | Γ ⊢ X : W}</td>
+            <td class="snns top italic magenta">typed abstraction</td>
+            <td class="snns top magenta">Γ ⊢ λW</td>
+            <td class="snns top magenta">no</td>
+            <td class="snns top magenta">&lt;W&gt;</td>
+            <td class="snns top magenta">(V)</td>
+            <td class="snns top magenta">#i</td>
+            <td class="ssns top magenta">→β *</td>
+          </tr>
+          <tr>
+            <td class="snns top">{X | Γ ⊢ X = V}</td>
+            <td class="snns top italic prune">abbreviation</td>
+            <td class="snns top prune">Γ ⊢ δV</td>
+            <td class="snns top prune">yes</td>
+            <td class="snns top prune">no</td>
+            <td class="snns top prune">no</td>
+            <td class="snns top prune">#i</td>
+            <td class="ssns top prune">→δ</td>
+          </tr>
+          <tr>
+            <td class="snss top">no</td>
+            <td class="snss top italic blue">sort</td>
+            <td class="snss top blue">Γ ⊢ ⋆k</td>
+            <td class="snss top blue">no</td>
+            <td class="snss top blue">no</td>
+            <td class="snss top blue">no</td>
+            <td class="snss top blue">no</td>
+            <td class="ssss top blue">no</td>
+          </tr>
+        </tbody>
+      </table>
+    </div>
+    <div xmlns:ld="http://lambdadelta.info/" class="text">* In terms only.
+   </div>
     <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="summary">Summary of the Specification <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b6.png" />
     </div>
     <div xmlns:ld="http://lambdadelta.info/" class="text">Here is a numerical account of the specification's contents
@@ -146,18 +196,18 @@
             <td class="snns italic cyan">files</td>
             <td class="snnn right italic cyan">120</td>
             <td class="snns italic cyan">characters</td>
-            <td class="snnn right italic cyan">198123</td>
+            <td class="snnn right italic cyan">198089</td>
             <td class="snns italic cyan">nodes</td>
             <td class="ssnn right italic cyan" />
           </tr>
           <tr>
             <td class="snns capitalize italic green">propositions</td>
             <td class="snns italic green">theorems</td>
-            <td class="snnn right italic green">699</td>
+            <td class="snnn right italic green">81</td>
             <td class="snns italic green">lemmas</td>
-            <td class="snnn right italic green">29</td>
+            <td class="snnn right italic green">618</td>
             <td class="snns italic green">total</td>
-            <td class="ssnn right italic green">728</td>
+            <td class="ssnn right italic green">699</td>
           </tr>
           <tr>
             <td class="snss capitalize italic yellow">concepts</td>
@@ -773,6 +823,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Mon, 19 Jan 2015 23:52:52 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 20 Jan 2015 18:39:00 +0100</div>
   </body>
 </html>
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html
index 2a6049ea6e891d943ed43d8a3456b5682f85dc06..b05d3b07d3f1bddd58c17ac40e071f3b13304621 100644 (file)
--- a/helm/www/lambdadelta/basic_2.html
+++ b/helm/www/lambdadelta/basic_2.html
@@ -1384,6 +1384,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Mon, 19 Jan 2015 23:52:52 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 20 Jan 2015 18:39:00 +0100</div>
   </body>
 </html>
diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html
index c49a38080e49eadf991ca3dd115db17cba709e20..2b7aee243ab97929199cf571d2b1dfc93bfb942a 100644 (file)
--- a/helm/www/lambdadelta/documentation.html
+++ b/helm/www/lambdadelta/documentation.html
@@ -366,6 +366,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Mon, 19 Jan 2015 23:52:51 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 20 Jan 2015 18:38:59 +0100</div>
   </body>
 </html>
diff --git a/helm/www/lambdadelta/download/lambdadelta_1.tar.gz b/helm/www/lambdadelta/download/lambdadelta_1.tar.gz
index 5a359df228b627c97bfe80f2456d2e9e32b118c4..6b0f832b8b514a49349cadc8d72e13804e31374e 100644 (file)
Binary files a/helm/www/lambdadelta/download/lambdadelta_1.tar.gz and b/helm/www/lambdadelta/download/lambdadelta_1.tar.gz differ
diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html
index 7d8d51b1324f8c41f6676abfcd814aac12c62785..92bd89f68894e1c0bb38b90012f260c5d578203a 100644 (file)
--- a/helm/www/lambdadelta/ground_2.html
+++ b/helm/www/lambdadelta/ground_2.html
@@ -297,6 +297,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Mon, 19 Jan 2015 23:52:51 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 20 Jan 2015 18:39:00 +0100</div>
   </body>
 </html>
diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html
index 8d832da50d9d52bf785e6d48fbe483ebeb4f71a9..5e06734647efc63f3673b510366e0e1c12b297d1 100644 (file)
--- a/helm/www/lambdadelta/implementation.html
+++ b/helm/www/lambdadelta/implementation.html
@@ -255,6 +255,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Mon, 19 Jan 2015 23:52:51 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 20 Jan 2015 18:38:59 +0100</div>
   </body>
 </html>
diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html
index c8641b1cb8bbf96a5eac6dcfc6b97572bb1b1fde..60ac77f4d88d1b5f67c8d171bff4bae61a8f8dd0 100644 (file)
--- a/helm/www/lambdadelta/index.html
+++ b/helm/www/lambdadelta/index.html
@@ -202,6 +202,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Mon, 19 Jan 2015 23:52:51 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 20 Jan 2015 18:38:59 +0100</div>
   </body>
 </html>
diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html
index 9bbcede0c0257313d3960b4e3ee1fa573c02cd06..2d4bbb7a99ae1ae3006a36430746e901b4fdc637 100644 (file)
--- a/helm/www/lambdadelta/news.html
+++ b/helm/www/lambdadelta/news.html
@@ -335,6 +335,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Mon, 19 Jan 2015 23:52:50 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 20 Jan 2015 18:38:59 +0100</div>
   </body>
 </html>
diff --git a/helm/www/lambdadelta/specification.html b/helm/www/lambdadelta/specification.html
index 6402c6fe42ae2d1d76b0239fd4d70b770a8eeb9f..47b54eed9457a7cc8c3526bc4df2ca8954df740f 100644 (file)
--- a/helm/www/lambdadelta/specification.html
+++ b/helm/www/lambdadelta/specification.html
@@ -327,6 +327,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Mon, 19 Jan 2015 23:52:51 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 20 Jan 2015 18:39:00 +0100</div>
   </body>
 </html>
Unnamed repository; edit this file 'description' to name the repository.