X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fwww%2Flambdadelta%2Fground_2.html;h=e5218996f8e362497548f1df7f8acb5b337263e0;hb=04ffe68396b98bbf21bcd403ffba03b94eaebadc;hp=8100642108138aec675bfd7613814157a6306fec;hpb=644307df315b855c3851f813b04d562acf2db9bc;p=helm.git
diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html
index 810064210..e5218996f 100644
--- a/helm/www/lambdadelta/ground_2.html
+++ b/helm/www/lambdadelta/ground_2.html
@@ -6,8 +6,8 @@
-
-
Here is a numerical acount of the specification's contents
and its timeline.
- Nodes are counted according to the "intrinsinc complexity measure"
- [F. Guidi: "Procedural Representation of CIC Proof Terms"
- Journal of Automated Reasoning 44(1-2), Springer (February 2010),
- pp. 53-78].
The source files are grouped in planes
- according to the following table.
- Notation files covering the whole specification are provided.
- The notation for the relations or functions introduced in each file
- is shown in parentheses (? are placeholders).
+
Logical Structure of the Specification
![lambdadelta butterfly [spacer]](http://lambdadelta.info/images/b4.png)
+
+
This table reports the specification's components and their planes.
- plane |
- files |
-
+ | component |
+ plane |
+ files |
+
|
-
+ |
|
-
+ |
|
-
+ |
|
-
+ |
|
-
+ |
|
-
+ |
|
-
+ |
|
- natural numbers with infinity |
- ynat ( â ) |
- ynat_pred ( â«°? ) |
- ynat_succ ( ⫯? ) |
- ynat_le ( ?� ) |
- ynat_lt ( ?<? ) |
- ynat_minus ( ? - ? ) |
- ynat_plus ( ? + ? ) |
- ynat_max |
- ynat_min |
+ natural numbers with infinity |
+ |
+ ynat ( â ) |
+ ynat_pred ( â«°? ) |
+ ynat_succ ( ⫯? ) |
+ ynat_le ( ? ⤠? ) |
+ ynat_lt ( ? < ? ) |
+ ynat_minus ( ? - ? ) |
+ ynat_plus ( ? + ? ) |
+ ynat_max |
+ ynat_min |
- extensions to the library |
- arith.ma ( ?^? ) |
-
-
- |
-
-
- |
-
+ | extensions to the library |
+ |
+ star |
+ lstar |
+ bool ( â» ) ( â ) |
+ arith ( ?^? ) |
+ list ( â ) ( ? @ ? ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| ) |
+
|
-
+ |
|
-
+ |
|
-
-
- |
-
-
- |
-
+ |
|
- generated logical decomposables |
- xoa ( ââ ) ( â¨â¨ ) ( â§â§ ) |
- xoa_props ( ⥠) ( ⤠) |
-
+ | generated logical decomposables |
+ |
+ xoa ( ââ ) ( â¨â¨ ) ( â§â§ ) |
+ xoa_props ( ⥠) ( ⤠) |
+
|
-
+ |
|
-
+ |
|
-
+ |
|
-
+ |
|
-
+ |
|
-
+ |
|
@@ -204,10 +262,6 @@
-
Physical Structure of the Specification
-
The source files are grouped in directories,
- one for each plane.
-
@@ -234,6 +288,6 @@
-
Last update: Sun, 20 Jul 2014 15:02:32 +0200
+
Last update: Tue, 04 Nov 2014 16:28:52 +0100