Date: Mon, 12 Dec 2011 17:10:51 +0000 (+0000) Subject: - we improved and updated the generated web pages X-Git-Tag: make_still_working~2024 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8344b3062fc040a7565e43b646d12197d1d51ee3;p=helm.git - we improved and updated the generated web pages --- diff --git a/helm/www/lambda_delta/ld_basic_2.html b/helm/www/lambda_delta/ld_basic_2.html index 41d3bf750..d6c6b3fe5 100644 --- a/helm/www/lambda_delta/ld_basic_2.html +++ b/helm/www/lambda_delta/ld_basic_2.html @@ -16,9 +16,9 @@

cic:/matita/lambda_delta/Basic_2/ (Î»Î´ version 2)

Logical structure of the contribution

The source files are grouped in planes and components according to the following table.

component	plane	files
examples
native typing		nty
conversion	context-sensitive conversion	cpcs
computation	strongly normalizing computation	lsubcs
		csn	csn_cr	csn_aarity
	context-sensitive computation	cprs
	support for abstract comptation properties	lsubc
		acp	acp_cr
reducibility	context-sensitive reduction	lcpr
		cpr	cpr_lift	cpr_ltpr	cpr_cpr
	context-free normal forms	twhnf	tnf
	context-free reduction	ltpr	ltpr_ldrop
		tpr	tpr_lift	tpr_tpss	tpr_tpr
	context-free reducible forms	trf
static typing	static type ass.	sty	sty_lift	sty_sty
	atomic arity ass.	aaa	aaa_lift	aaa_aaa
	parameters	sh
unfold	term inverse relocation	delift
	partial unfold	ltpss	ltpss_ldrop	ltpss_tps	ltpss_ltpss
		tpss	tpss_lift	tpss_tpss	tpss_ltps
substitution	parallel substitution	ltps	ltps_ldrop	ltps_tps	ltps_ltps
		tps	tps_lift	tps_tps
	local env. dropping	ldrop	ldrop_ldrop
	term relocation	lift	lift_lift
grammar	local env. ref. for substitution	lsubs	lsubs_lsubs
	term hom.	thom	thom_thom
	closures	cl_shift	cl_weight
	internal syntax	lenv	lenv_weight	lenv_length
		term	term_weight	term_simple
		item
	external syntax	aarity

component	plane	files
examples
native typing		nty
conversion	context-sensitive conversion	cpcs
computation	strongly normalizing computation	lsubcs
		csn	csn_cr	csn_aarity
	context-sensitive computation	cprs
	support for abstract comptation properties	lsubc
		acp	acp_cr
reducibility	context-sensitive reduction	lcpr
		cpr	cpr_lift	cpr_ltpr	cpr_cpr
	context-free normal forms	twhnf	tnf
	context-free reduction	ltpr	ltpr_ldrop
		tpr	tpr_lift	tpr_tpss	tpr_tpr
	context-free reducible forms	trf
static typing	static type ass.	sty	sty_lift	sty_sty
	atomic arity ass.	aaa	aaa_lift	aaa_aaa
	parameters	sh
unfold	term inverse relocation	delift
	partial unfold	ltpss	ltpss_ldrop	ltpss_tps	ltpss_ltpss
		tpss	tpss_lift	tpss_tpss	tpss_ltps
substitution	parallel substitution	ltps	ltps_ldrop	ltps_tps	ltps_ltps
		tps	tps_lift	tps_tps
	global env. slicing	gdrop
	local env. slicing	ldrop	ldrop_ldrop
	term relocation	lift	lift_lift
grammar	local env. ref. for substitution	lsubs	lsubs_lsubs
	term hom.	thom	thom_thom
	closures	cl_shift	cl_weight
	internal syntax	lenv	lenv_weight	lenv_length
		term	term_weight	term_simple
		item
	external syntax	aarity

Physical structure of the contribution

The source files are grouped in directories, one for each component.

Last update: 2011-12-12+01:00

diff --git a/helm/www/lambda_delta/web/home/ld_basic_2.tbl b/helm/www/lambda_delta/web/home/ld_basic_2.tbl index 503c11d45..97a97aaa9 100644 --- a/helm/www/lambda_delta/web/home/ld_basic_2.tbl +++ b/helm/www/lambda_delta/web/home/ld_basic_2.tbl @@ -109,7 +109,11 @@ table { [ "tps" "tps_lift" "tps_tps" * ] } ] - [ { "local env. dropping" * } { + [ { "global env. slicing" * } { + [ "gdrop" * ] + } + ] + [ { "local env. slicing" * } { [ "ldrop" "ldrop_ldrop" * ] } ] diff --git a/helm/www/lambda_delta/xslt/ld_web_root.xsl b/helm/www/lambda_delta/xslt/ld_web_root.xsl index 7a020ad46..8222e1d94 100644 --- a/helm/www/lambda_delta/xslt/ld_web_root.xsl +++ b/helm/www/lambda_delta/xslt/ld_web_root.xsl @@ -2,8 +2,10 @@ @@ -25,6 +27,8 @@ + +

@@ -32,7 +36,12 @@

+ +

+ + +