+
+ System and Specification
+ (updated ).
+
Informational pages on the specifications are provided.
The formal specification of λδ version 3
is forthcoming.
@@ -54,64 +61,91 @@
- λδ version 2 (active)
+ λδ version 2 (active)
The formal specification of λδ version 2
- is available in the following formats:
+ is available in the following formats.
-
-
- lambdadelta_2A1 for Matita 0.99.2
- (revised ).
- Source scripts.
- Documentation (R2c).
-
+
+ Informational pages on the parts of the specification:
+ Background,
+ Syntax,
+ Core,
+ Applications.
+
+
+
+
+ The scripts are grouped in directories, first by part, then by component.
+
+
+
+
+ the scripts are checked by the latest version of Matita from
+ HELM Git repository.
+
+
+
- The scripts are grouped in directories, first by part, then by component.
+ lambdadelta_2B for Matita 0.99.4
+ (revised ).
+ Source scripts [Git revision: 2019-11-19 20:45:15].
+ Documentation (J2a).
+
+
+
-
- the scripts are checked by the latest version of Matita from
- HELM Subversion repository
- at path <trunk/matita/>.
+ lambdadelta_2A for Matita 0.99.2
+ (revised ).
+ Source scripts [Git revision: 2014-10-28 17:46:26].
+ Documentation (R2c).
+
+
+ repackaging (was lambdadelta_2A1).
+
+
+
+ λδ version 1 (superseded)
- Informational pages on the parts of the specification:
- Background,
- Core,
- Applications.
+ The formal specification of λδ version 1
+ is available in the following formats.
-
+
+ Informational pages on the parts of the specification:
+ Background,
+ Core.
+
- λδ version 1 (superseded)
- The formal specification of λδ version 1
- is available in the following formats:
+
+ The scripts are grouped in directories, one for each part.
-
+
- lambdadelta_1 for Coq 7.3.1
- (revised ).
+ lambdadelta_1A for Coq 7.3.1
+ (revised ).
Source scripts.
- Documentation (J1a).
+ Documentation (J1a).
+
+ repackaging (was lambdadelta_1).
+
17 new lemmas and former lemma "eq_nat_dec" renamed as "nat_dec_neg".
-
- The scripts are grouped in directories, one for each part.
-
-
- lambdadelta_1 for Matita 0.5
- (revised ).
+
+ lambdadelta_1A for Matita 0.5
+ (revised ).
Static HTML pages generated by the HELM rendering engine.
@@ -135,19 +169,13 @@
-
+
- lambdadelta_1 for Matita 0.5
- (revised ).
+ lambdadelta_1A for Matita 0.5
+ (revised ).
HELM directory.
-
- Informational pages on the parts of the specification:
- Background,
- Core.
-
-