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=e4499a294b2793272e787a5f56417a7adc97c3de;hb=c60524dec7ace912c416a90d6b926bee8553250b;hp=f13d943f893367f9983885a841e0c15cc900f8e9;hpb=f10cfe417b6b8ec1c7ac85c6ecf5fb1b3fdf37db;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 f13d943f8..e4499a294 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 @@ -10,32 +10,30 @@ applications of λδ version 2. In particular it contains the components below. - - Martin-Löf's Type Theory with one universe - using λδ as theory of expressions. - - - The validation algorithm for λδ as implemented in - Helena 0.8. - + + + Martin-Löf's Type Theory with one universe + using λδ as theory of expressions. + + + + The validation algorithm for λδ as implemented in + 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]. - + The Applications directory is started. - + The Functional component is started inside the specification of λδ version 2. - + The MLTT1 component is started. @@ -48,9 +46,5 @@
-
Physical Structure of the Specification
- The source files are grouped in directories, - one for each component. -