Date: Sun, 25 Dec 2011 19:52:48 +0000 (+0000) Subject: Basic 2 page update X-Git-Tag: make_still_working~1997 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=30df7ebabc6eb145c28a9724c6e8ad9612c784b1;p=helm.git Basic 2 page update --- diff --git a/helm/www/lambda_delta/ld_basic_2.html b/helm/www/lambda_delta/ld_basic_2.html index e66d370ee..8e4dca575 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
functional	unfold	lift	subst
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	delift_lift
	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

component	plane	files
functional	unfold	lift	subst
examples
native typing		nty
conversion	context-sensitive conversion	cpcs
computation	strongly normalizing computation	csn	csn_cr	csn_aaa
	context-sensitive computation	cprs
	support for abstract computation properties	lsubc
		acp	acp_cr	acp_aaa
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	delift_lift
	partial unfold	ltpss	ltpss_ldrop	ltpss_tps	ltpss_ltpss
		tpss	tpss_lift	tpss_tpss	tpss_ltps
	generic local env. slicing	lifts	ldrops
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	lift_vector
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	term_vector
		item
	external syntax	aarity

Physical structure of the contribution

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

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

Last update: 2011-12-25+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 89cc5e535..5ef4c8603 100644 --- a/helm/www/lambda_delta/web/home/ld_basic_2.tbl +++ b/helm/www/lambda_delta/web/home/ld_basic_2.tbl @@ -44,17 +44,16 @@ table { class "water" [ { "computation" * } { [ { "strongly normalizing computation" * } { - [ "lsubcs" * ] - [ "csn" "csn_cr" "csn_aarity" * ] + [ "csn" "csn_cr" "csn_aaa" * ] } ] [ { "context-sensitive computation" * } { [ "cprs" * ] } ] - [ { "support for abstract comptation properties" * } { + [ { "support for abstract computation properties" * } { [ "lsubc" * ] - [ "acp" "acp_cr" * ] + [ "acp" "acp_cr" "acp_aaa" * ] } ] } @@ -108,6 +107,10 @@ table { [ "tpss" "tpss_lift" "tpss_tpss" "tpss_ltps" * ] } ] + [ { "generic local env. slicing" * } { + [ "lifts" "ldrops" * ] + } + ] } ] class "orange" @@ -126,7 +129,7 @@ table { } ] [ { "term relocation" * } { - [ "lift" "lift_lift" * ] + [ "lift" "lift_lift" "lift_vector" * ] } ] } @@ -147,7 +150,7 @@ table { ] [ { "internal syntax" * } { [ "lenv" "lenv_weight" "lenv_length" * ] - [ "term" "term_weight" "term_simple" * ] + [ "term" "term_weight" "term_simple" "term_vector" * ] [ "item" * ] } ]