Contents of the Specification [spacer]

Contents of the Specification $\lambda\delta butterfly$

This specification comprises a collection of checked applications of Î»Î´ version 2. @@ -122,7 +122,13 @@ Helena 0.8. -

Summary of the Specification [spacer]

+ Examples. + Terms of Î»Î´ with special features. +

Summary of the Specification $\lambda\delta butterfly$

Here is a numerical account of the specification's contents and its timeline. @@ -152,33 +158,39 @@ sizes files - 14 + 1 characters - 6787 + 377 nodes - 10070 + 779 propositions theorems 2 lemmas - 4 + 1 total - 6 + 3 concepts declared - 6 + 0 defined - 11 + 3 total - 17 + 3

+ 2017 March 6. + The Examples component is moved from the Core directory. +

2012 February 24. @@ -198,7 +210,7 @@ The MLTT1 component is started.

Logical Structure of the Specification [spacer]

Logical Structure of the Specification $\lambda\delta butterfly$

This table reports the specification's components and their planes.

@@ -214,17 +226,25 @@ - functional - reduction and type machine - rtm - rtm_step ( ? â¨ ? ) + functional + reduction and type machine + rtm + rtm_step ( ? â¨ ? ) - +
- relocation - lift ( â[?,?] ? ) + relocation + lift ( â[?,?] ? ) + +
+ + + + examples + terms with special features + ex_sta_ldec ex_cpr_omega ex_fpbg_refl ex_snv_eta
@@ -233,7 +253,7 @@

+ $\lambda\delta rainbow rule$

@@ -258,6 +278,6 @@

Last update: Fri, 06 Mar 2015 17:53:24 +0100

Last update: Sat, 01 Apr 2017 16:50:39 +0200