X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=8507922549e11f63c891184bf90cde259161f908;hb=0c7129d74ba0bfbdf7f71ffcf46a8c8c93e7df14;hp=eb181a3ee3f03ecdb06c2591641e3997f9c7a045;hpb=cc072ef7058246bbc0deaf3e44a75b0e5977df65;p=helm.git diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index eb181a3ee..850792254 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,116 +23,15 @@
[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
Here is a numerical acount of the specification's contents and its timeline. + Nodes are counted according to the "intrinsinc complexity measure" + [F. Guidi: "Procedural Representation of CIC Proof Terms" + Journal of Automated Reasoning 44(1-2), Springer (February 2010), + pp. 53-78].
@@ -159,29 +58,29 @@ - + - + - - + - + - + - + - + - +
sizes files252361 characters483453651755 nodes + 1819305
propositions theorems85121 lemmas11191293 total12041414
concepts declared4654 defined8281 total128135
@@ -195,18 +94,68 @@ + + + + + + +