X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=68f455388549923329a0a6a8a2c8cb231e4dc59b;hb=bb1a03359dfaea6031592d28b9bfb15d797c44e5;hp=213361156cc4e314d71732153db184866c547dbe;hpb=265f584ad05c29694376127e46aef45cc546d43c;p=helm.git diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index 213361156..68f455388 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,9 @@
[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,54 +37,56 @@ - - - + + - - - - - - - - - - - + + + + + + + - - - - - - - + + + + + + + - - - - - - - + + + + + + +
categoryobjects + categoryobjects
+
+
+
+
sizesfiles298 characters466817nodes1359471sizesfiles359characters429712nodes1856521
propositionstheorems89lemmas910total999propositionstheorems127lemmas1273total1400
conceptsdeclared50defined73total123conceptsdeclared54defined83total137
+ +
Stage "B"
+ +
Stage "A": "Weakening the Applicability Condition"
+ + + +