X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fwww%2Flambdadelta%2Fground_2.html;h=94be6097921cb578b4aaee1beca22acf72f081c8;hb=d21e43252fea9aa0351824525014a2471b7bd232;hp=6c4c190f77c94bbdea944c6ea8b7b7a56b06ecf5;hpb=a5d21c8955339a48f28c22e0c3cfe43363d39188;p=helm.git
diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html
index 6c4c190f7..94be60979 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
+
+
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 ( ? + ? ) |
+ 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 ( ⥠) ( ⤠) |
-
+ |
|
-
+ |
|
-
+ |
|
-
+ |
|
-
+ |
|
@@ -184,10 +262,6 @@
-
Physical Structure of the Specification
-
The source files are grouped in directories,
- one for each plane.
-
@@ -214,6 +288,6 @@
-
Last update: Wed, 04 Dec 2013 16:42:13 +0100
+
Last update: Tue, 04 Nov 2014 16:21:23 +0100