X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fapps_2%2Fweb%2Fapps_2.ldw.xml;h=dac657eb326a2e9e51d7dd33dd6c0b511194bc36;hb=cfc43911db215e21036317b26bd1dcf9c3e5d435;hp=394568e00b0a750cb78b38e1015d9eb4bf5a17ed;hpb=037b48dbbc0b4373ad1e43d837ac9158787486ef;p=helm.git
diff --git a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml
index 394568e00..dac657eb3 100644
--- a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml
+++ b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml
@@ -8,20 +8,24 @@
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.
Martin-Löf's Type Theory with one universe
- using λδ as theory of expressions.
+ using λδ as theory of expressions.
The validation algorithm for λδ as implemented in
- Helena 0.8.
+ Helena 0.8.
-
+
Summary of the Specification
Here is a numerical acount 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].
@@ -29,7 +33,7 @@
The Functional component is started
- inside the specification of λδ version 2.
+ inside the specification of λδ version 2.
The MLTT1 component is started.
@@ -39,8 +43,8 @@
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).