X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=12764cede0458a9d7dffbfc96af921a00c923e46;hb=5275f55f5ec528edbb223834f3ec2cf1d3ce9b84;hp=3824bbef7aa502f3bdf51689171eb1aded338d6b;hpb=29b8894621ee2f91f9582e9d2bd88913961b1df0;p=helm.git diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index 3824bbef7..12764cede 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -1,88 +1,692 @@ - + - - - - - - lambdadelta version 2 - - - - + + + + + + \lambda\delta home page + + + + -
[lambdadelta home]
cic:/matita/lambdadelta/basic_2/ (λδ version 2)
[Spacer]
-
System's Syntax and Behavior
-
This is a summary of the "block structure" + +
+ + [\lambda\delta home] + +
+
cic:/matita/lambdadelta/basic_2/ (core λδ version 2)
+
+ [Spacer] +
+
+
+
+
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+ home + + news + + specification + +
+ 		+
+ 		+ documentation + + implementation + +
+
+ foreword + + milestones + + version 2 + (background - core - applications) +
+ 		+ version 2 + + helena + +
+
+ citations + + visibility + + version 1 + (background - core)(static HELM directory) + version 1 + + library + (static LDDL directory)
+
+ +
Summary of the Specification [spacer] +
+
Here is a numerical account of the specification's contents and its timeline.
-
categoryobjects




sizesfiles242characters464527nodes1269595
propositionstheorems83lemmas1068total1151
conceptsdeclared42defined78total120
- + +
Logical Structure of the Specification [spacer] +
+
This table reports the specification's components and their planes.
-
[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-18T20:41:26+01:00
- +
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
componentplanefiles +
+ 		+
+ 		+
+
static typingparametersshsd +
+ 		+
+
+
+ 		restricted ref. for local env.lsubr ( ? ⫃ ? )lsubr_length lsubr_drops lsubr_lsubr +
+ 		+
+
+
+ 		ranged equivalence for closuresfreq ( ⦃?,?,?⦄ ≡ ⦃?,?,?⦄ )freq_freq +
+ 		+
+
+
+ 		context-sensitive free variablesfrees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? )frees_weight frees_lreq frees_frees +
+ 		+
+
s-computation + +
+ 		+
+ 		+
+ 		+
+
s-transitionstructural successor for closuresfquq ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ )fquq_length fquq_weight +
+ 		+
+
+
+ 		+
+ 		fqu ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ )fqu_length fqu_weight +
+ 		+
+
relocationgeneric slicing for local environmentsdrops_vector ( ⬇*[?,?] ? ≡ ? ) +
+ 		+
+ 		+
+
+
+ 		+
+ 		drops ( ⬇*[?,?] ? ≡ ? )drops_lstar drops_weight drops_length drops_ceq drops_lexs drops_lreq drops_drops +
+ 		+
+
+
+ 		generic relocation for termslifts_vector ( ⬆*[?] ? ≡ ? )lifts_lifts_vector +
+ 		+
+
+
+ 		+
+ 		lifts ( ⬆*[?] ? ≡ ? )lifts_simple lifts_weight lifts_lifts +
+ 		+
+
+
+ 		ranged equivalence for local environmentslreq ( ? ≡[?] ? )lreq_length lreq_lreq +
+ 		+
+
+
+ 		generic entrywise extension of context-sensitive relations for termalexs ( ? ⦻*[?,?,?] ? )lexs_length lexs_lexs +
+ 		+
+
grammarappend for local environmentsappend ( ? @@ ? )append_length +
+ 		+
+
+
+ 		context-sensitive equivalences for termsceqceq_ceq +
+ 		+
+
+
+ 		same top term structuretsts ( ? ≂ ? )tsts_tsts tsts_vector +
+ 		+
+
+
+ 		closurescl_weight ( ♯{?,?,?} )cl_restricted_weight ( ♯{?,?} ) +
+ 		+
+
+
+ 		internal syntaxgenv +
+ 		+
+ 		+
+
+
+ 		+
+ 		lenvlenv_weight ( ♯{?} )lenv_length ( |?| ) +
+
+
+ 		+
+ 		termterm_weight ( ♯{?} )term_simple ( 𝐒⦃?⦄ )term_vector ( Ⓐ?.? )
+
+ 		+
+ 		item +
+ 		+
+ 		+
+
+
+ 		external syntaxaarity +
+ 		+
+ 		+
+
+
+
+ [Spacer] +
+
+
+
+
+ + [Valid XHTML 1.1] + + + [Valid CSS level 2] + + + [Generated from XML via XSL] + + + [PNG used here] + + + [Viewable with any browser] + +
+
+
+
+
Last update: Thu, 07 Apr 2016 15:45:52 +0200
+