+
Notice:
the scripts are checked by the latest version of Matita from
HELM Subversion repository
at path <trunk/matita/>.
+
Informational pages on the parts of the specification:
Background,
Core,
Applications.
-
- Notice on numerical acounts:
- nodes are counted according to the "intrinsic complexity measure"
- [F. Guidi: "Procedural Representation of CIC Proof Terms"
- Journal of Automated Reasoning 44(1-2), Springer (February 2010), pp. 53-78].
-
-
- Notice on displayed logical structures:
- from the logical standpoint, the source scripts are grouped in "planes"
- and these are grouped in "components";
- the notation for the relations or functions
- introduced in each script, is shown in parentheses (? are placeholders).
-
-
-
-
-
+
+
λδ version 1 (superseded)
-
+
The formal specification of λδ version 1
is available in the following formats:
-
-
+
-
-
-
lambdadelta_1 for Coq 7.3.1
- (revised
2012-10).
+
+
lambdadelta_1 for Coq 7.3.1
+ (revised
2015-09).
Source scripts.
-
-
+
+ -
+ 2015 January 15.
+ 17 new lemmas and former lemma "eq_nat_dec" renamed as "nat_dec_neg".
+
+
+
+
The scripts are grouped in directories, one for each part.
-
+
-
-
+
-
-
+
-
-
+
+ Informational pages on the parts of the specification:
+
Background,
+
Core.
+
+
@@ -309,6 +328,6 @@
-
Last update: Sat, 01 Nov 2014 17:50:21 +0100
-