X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=f00ca8e1a767ad574c21dacc0b23716b23c9d0b5;hb=f8bf3abd773864388fef5efe599ac77f292a6b9d;hp=dbd2291ad9ddf40a6f4bd677c862f97fcb2af10f;hpb=22ff568044ad894d0e2a48bae84c13f95ee2d637;p=helm.git diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index dbd2291ad..f00ca8e1a 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -6,8 +6,8 @@ - - lambdadelta version 2 + + \lambda\delta version 2 @@ -23,114 +23,10 @@
[Spacer]
-
System's Syntax and Behavior
-
This is a summary of the "block structure" - of the System's syntactic items and reductions. -
-
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
domainblockleaderapplicator (with →θ)*reduction→ζ *reference *
{X | Γ ⊢ X : W}local typed abstraction *Γ ⊢ +λWⓐV→βno#i
-
- 		local typed declaration **Γ ⊢ -λWⓐV→βno#i
-
- 		global typed declaration ***Γ ⊢ pλWnonono$p
-
- 		native type annotation *Γ ⊢ ⓝWnonoyesno
{X | Γ ⊢ X = V}local abbreviation *Γ ⊢ +δVnolocal →δyes#i
-
- 		local definition **Γ ⊢ -δVnolocal →δno#i
-
- 		global definition ***Γ ⊢ pδVnoglobal →δno$p
nosort ****Γ ⊢ ⋆knononono
-
-
* In terms only. - ** In terms and local environments only. - *** In global environments only. - **** Sort level k in terms only. -
-
Summary of the Specification
+ + +
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" @@ -142,50 +38,50 @@ - - - + + - - - - - + - + - + - + - + - + - + - + - +
categoryobjects + categoryobjects
+
+
+
+
sizes files301 362 characters472212430997 nodes13931331829107
propositions theorems89123 lemmas9131300 total10021423
concepts declared5054 defined7384 total123138
@@ -199,9 +95,32 @@ + + +