X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fapps_2.html;h=ece3b07ca811216589804886307c210ebe7c0d86;hb=9b1b59a049935f5382ed7def91b807bbf9453894;hp=9d22358fa29ba75ffd8999fbc2c0eb2f29fc9b95;hpb=03e9a07b37a7e372f8ee88071b05bd3f49a0b368;p=helm.git diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index 9d22358fa..eb3ac6cda 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -1,62 +1,261 @@ - + - - - - - - applications of lambdadelta version 2 - - - - + + + + + + \lambda\delta home page + + + + -
[lambdadelta home]
cic:/matita/lambdadelta/apps_2/ (applications of λδ version 2)
[Spacer]
-
Contents of the Specification
-
This specification comprises a collection of checked + +
+ + [\lambda\delta home] + +
+
cic:/matita/lambdadelta/apps_2/ (applications of λδ version 2)
+
+ [Spacer] +
+
+
+
+
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+ home + + news + + specification + +
+ 		+
+ 		+ documentation + + implementation + +
+
+ foreword + + milestones + + version 2 + (background - core - applications) +
+ 		+ version 2 + + helena + + Open Symbolic Notation (OSN) +
+ citations + + visibility + + version 1 + (background - core)(static HELM directory) + version 1 + + library + (static LDDL directory)
+
+
Contents of the Specification [butterfly] +
+
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 + + + +
Summary of the Specification [butterfly] +
+
Here is a numerical account of the specification's contents and its timeline.
-
-
  • 2012 February 24. +
    + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    categoryunits +
    +     		+
    +     		+
    +     		+
    +     		+
    +
    sizescharacters (files)377 (1)nodes (objects)779 (6)intrinsic loss factor2.1
    propositionstheorems2lemmas1total3
    conceptsdeclared0defined3total3
    +
    +
      +
    • + 2017 March 6. + The Examples component is moved from the Core directory. +
      • +
    +
      +
    • + 2012 February 24. The Applications directory is started. -
    -
    • 2011 December 20. +
      • +
    +
      +
    • + 2011 December 20. The Functional component is started - inside the specification of λδ version 2. -
    -
    • 2011 December 12. + inside the specification of λδ version 2. +
      • +
    +
      +
    • + 2011 December 12. The MLTT1 component is started. -
    - -
    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). +
    • +
+
Logical Structure of the Specification [butterfly] +
+
This table reports the specification's components and their planes.
-
componentplanefiles
MLTT1genv_primitivejudgement
functionalreduction and type machinertmrtm_step ( ? ⇨ ? )

unfoldlift ( ↑[?,?] ? )subst ( [?←?] ? )
- -
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-07T20:49:53+01:00
- +
+ + + + + + + + + + + + + +
componentplanefiles
examplesterms with special featuresex_cpr_omega
+
+
+ [Spacer] +
+
+
+
+
+ + [Valid XHTML 1.1] + + + [Valid CSS level 2] + + + [Generated from XML via XSL] + + + [PNG used here] + + + [Viewable with any browser] + +
+
+
+
+
Last update: Fri, 24 Nov 2017 21:00:01 +0100
+