X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fapps_2.html;h=9d03180c2b18bc1a51fac81cd7a474d503c0727d;hb=3fb2d167ba8463e0fa80efe42ee9be1a15e282a0;hp=8b513c2633c12ffecc50ebe4a266f5f3c2c10ba4;hpb=1748969db46c372d20be316e41737cd206129205;p=helm.git diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index 8b513c263..9d03180c2 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -1,62 +1,204 @@ - + - - - - - + + + + + applications of lambdadelta version 2 - - - - + + + + -
[lambdadelta home]
cic:/matita/lambdadelta/apps_2/ (applications of λδ version 2)
[Spacer]
-
Contents of the Specification
-
This specification comprises a collection of checked + +
+ + [lambdadelta home] + +
+
cic:/matita/lambdadelta/apps_2/ (applications of λδ version 2)
+
+ [Spacer] +
+
Contents of the Specification
+
This specification comprises a collection of checked applications of λδ version 2. - In particular it contains the components below. + In particular it contains the components below.
- + +
Summary of the Specification
+
Here is a numerical acount of the specification's contents and its timeline.
-
categoryobjects




sizesfiles5characters5613nodes10024
propositionstheorems4lemmas1total5
conceptsdeclared3defined10total13
- -
Logical Structure of the Specification
-
The source files are grouped in planes and components +
Logical Structure of the Specification
+
The source files are grouped in planes and components according to the following table. Each component contains its own notation file. - The notation for the relations or functions introduced in each file - is shown in parentheses (? are placeholders). + The notation for the relations or functions introduced in each file + is shown in parentheses (? are placeholders).
-
componentplanefiles
MLTT1genv_primitivejudgement
functionalreduction and type machinertmrtm_step ( ? ⇨ ? )

unfoldlift ( ↑[?,?] ? )subst ( [?←?] ? )
+
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
componentplanefiles +
+
MLTT1 + genv_primitivejudgement
functionalreduction and type machinertmrtm_step ( ? ⇨ ? )
+
+ 		unfoldlift ( ↑[?,?] ? )subst ( [?←?] ? )
examples + + +
+
+
-
Physical Structure of the Specification
-
The source files are grouped in directories, +
Physical Structure of the Specification
+
The source files are grouped in directories, one for each component.
-
[Spacer]

[Valid XHTML 1.1][Valid CSS level 2][Generated from XML via XSL][PNG used here][Viewable with any browser]

Last update: 2013-02-01T19:32:03+01:00
+
+ [Spacer] +
+
+
+
+
+ + [Valid XHTML 1.1] + + + [Valid CSS level 2] + + + [Generated from XML via XSL] + + + [PNG used here] + + + [Viewable with any browser] + +
+
+
+
+
Last update: Sun, 07 Apr 2013 23:37:36 +0200