+
+
+ +
+
+
+
+
+ + home + | ++ news + | ++ documentation + | ++ specification + | +
+ + |
+
+ + |
+ + implementation + | +
+ + |
+
+ foreword + | ++ milestones + | ++ version 2 + | ++ version 2 + | +(background - core - applications) | +
+ + |
+ + library + | +(static LDDL directory) | +
+ citations + | ++ visibility + | ++ version 1 + | ++ version 1 + | +(background - core) | +(static HELM directory) | ++ helena + | +
+ + |
+
Summary of the Specification
+
+ ![lambdadelta butterfly [spacer]](http://lambdadelta.info/images/b4.png)
Here is a numerical account 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].
-
+
-
files | 30 | characters | -68581 | +46649 | nodes | 62380 |
-
+
- - 2013 November 27. + 2013 November 27. Natural numbers with infinity.
- - 2011 August 10. + 2011 August 10. Specification starts.
-
+
Logical Structure of the Specification
- 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.
-
+
-
-
component | plane | files | @@ -135,23 +208,44 @@ | |||||||||||||||||
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 ( ⥠) ( ⤠) |
|
@@ -175,9 +269,14 @@
||||||||||||||||
generated logical decomposables | -xoa ( ââ ) ( â¨â¨ ) ( â§â§ ) | -xoa_props ( ⥠) ( ⤠) | ++ | + |
+ + |
+
+ + |
|
@@ -203,12 +302,7 @@
Physical Structure of the Specification
- The source files are grouped in directories,
- one for each plane.
-
-
+
![lambdadelta rainbow rule [Spacer]](http://lambdadelta.info/images/rainbow.png)
@@ -234,6 +328,6 @@
-
Last update: Mon, 20 Oct 2014 16:17:00 +0200
-