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 [Svn revision: 12964].
- Documentation (R2c).
-
-
- The scripts are grouped in directories, first by part, then by component.
-
-
-
- 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,
@@ -87,33 +69,77 @@
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.
+
+
+
+
+ lambdadelta_2B for Matita 0.99.4
+ (revised ).
+ Source scripts [Git revision: 2019-11-19 20:45:15].
+ Documentation (V2b).
+
+
+
+
+
+ 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)
The formal specification of λδ version 1
- is available in the following formats:
+ is available in the following formats.
-
+
+ Informational pages on the parts of the specification:
+ Background,
+ Core.
+
+
+
+
+ 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).
+
+ 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.
@@ -137,19 +163,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.
-
-