X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fapps_2.html;h=a0d1206ed676dae1b6c0411b90e99c22ed721419;hb=f7d7f2459b3b0409be5f168822be3b836ccc929b;hp=31b4d9c92322a4593cec95fbf96c90395883265d;hpb=7562d9781dc4f351ddc3b2f8edd21f4976621948;p=helm.git diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index 31b4d9c92..a0d1206ed 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -23,7 +23,7 @@
[Spacer]
-
+

@@ -36,18 +36,24 @@ news + + specification + + +
+ + +
+ documentation - specification + implementation - +
- - implementation - @@ -56,16 +62,20 @@ milestones + + version 2 + + (background - core - applications) + +
+ version 2 - version 2 - - (background - core - applications) - library + (static LDDL directory) @@ -74,50 +84,50 @@ visibility + + version 1 + + (background - core) + (static HELM directory) version 1 - version 1 + helena - +
- - helena -
- -
Contents of the Specification [spacer] +
Contents of the Specification [spacer]
-
This specification comprises a collection of checked +
This specification comprises a collection of checked applications of λδ version 2. In particular it contains the components below.
-
    +
    • - MLTT1. + MLTT1. Martin-Löf's Type Theory with one universe using λδ as theory of expressions.
    -
      +
      • - Functional. + Functional. The validation algorithm for λδ as implemented in Helena 0.8.
      - -
      Summary of the Specification [spacer] +
      Summary of the Specification [spacer]
      -
      Here is a numerical acount of the specification's contents +
      Here is a numerical account of the specification's contents and its timeline.
      -
      +
      @@ -142,58 +152,57 @@ - + - + - + - + - + - + - + - + - +
      sizes files41 characters68581217 nodes36370
      propositions theorems20 lemmas10 total30
      concepts declared30 defined90 total120
      -
        +
        • 2012 February 24. The Applications directory is started.
        -
          +
          • 2011 December 20. The Functional component is started inside the specification of λδ version 2.
          -
            +
            • 2011 December 12. The MLTT1 component is started.
            - -
            Logical Structure of the Specification [spacer] +
            Logical Structure of the Specification [spacer]
            -
            This table reports the specification's components and their planes. +
            This table reports the specification's components and their planes.
            -
            +
            @@ -223,8 +232,7 @@
            - -
            +
            [Spacer]
            @@ -250,6 +258,6 @@

            -
            Last update: Tue, 04 Nov 2014 16:28:52 +0100
            - +
            Last update: Fri, 01 Apr 2016 23:30:52 +0200
            +