Date: Mon, 14 Nov 2011 17:22:11 +0000 (+0000) Subject: file names and description update X-Git-Tag: make_still_working~2115 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=eaaba018b368be3410b6d966dde578af46064ec0;p=helm.git file names and description update --- diff --git a/helm/www/lambda_delta/ld_basic_2.html b/helm/www/lambda_delta/ld_basic_2.html index dab3a5e30..142598d2c 100644 --- a/helm/www/lambda_delta/ld_basic_2.html +++ b/helm/www/lambda_delta/ld_basic_2.html @@ -16,7 +16,7 @@

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	cpcs
computation	strongly normalizing	csn
	context-sensitive	cprs
reducibility	context-sensitive reduction	lcpr
		cpr	cpr_lift	cpr_ltpr	cpr_cpr
	context-free normal forms	tnf
	context-free reduction	ltpr	ltpr_ldrop
		tpr	tpr_lift	tpr_tpss	tpr_tpr
	context-free reducible forms	trf
static typing	atomic arity ass.	aaa	aaa_lift	aaa_aaa
	static type ass.	sty	sty_lift	sty_sty
unfold	partial	ltpss	ltpss_ldrop	ltpss_tps	ltpss_ltpss
		tpss	tpss_lift	tpss_tpss	tpss_ltps
substitution	parallel	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
	parameters	sh

component	plane	files
examples
native typing		nty
conversion	context-sensitive conversion	cpcs
computation	strongly normalizing computation	csn
	context-sensitive computation	cprs
reducibility	context-sensitive reduction	lcpr
		cpr	cpr_lift	cpr_ltpr	cpr_cpr
	context-free normal forms	tnf
	context-free reduction	ltpr	ltpr_ldrop
		tpr	tpr_lift	tpr_tpss	tpr_tpr
	context-free reducible forms	trf
static typing	atomic arity ass.	aaa	aaa_lift	aaa_aaa
	static type ass.	sty	sty_lift	sty_sty
unfold	telescopic substitution	tsubst
	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
	parameters	sh

Physical structure of the contribution

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

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 0d0518140..bcbb90b8b 100644 --- a/helm/www/lambda_delta/web/home/ld_basic_2.tbl +++ b/helm/www/lambda_delta/web/home/ld_basic_2.tbl @@ -27,7 +27,7 @@ table { ] class "cyan" [ { "conversion" * } { - [ { "context-sensitive" * } { + [ { "context-sensitive conversion" * } { [ "cpcs" * ] } ] @@ -35,11 +35,11 @@ table { ] class "water" [ { "computation" * } { - [ { "strongly normalizing" * } { + [ { "strongly normalizing computation" * } { [ "csn" * ] } ] - [ { "context-sensitive" * } { + [ { "context-sensitive computation" * } { [ "cprs" * ] } ] @@ -81,7 +81,11 @@ table { ] class "yellow" [ { "unfold" * } { - [ { "partial" * } { + [ { "telescopic substitution" * } { + [ "tsubst" * ] + } + ] + [ { "partial unfold" * } { [ "ltpss" "ltpss_ldrop" "ltpss_tps" "ltpss_ltpss" * ] [ "tpss" "tpss_lift" "tpss_tpss" "tpss_ltps" * ] } @@ -90,7 +94,7 @@ table { ] class "orange" [ { "substitution" * } { - [ { "parallel" * } { + [ { "parallel substitution" * } { [ "ltps" "ltps_ldrop" "ltps_tps" "ltps_ltps" * ] [ "tps" "tps_lift" "tps_tps" * ] }