X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambda_delta%2Fld_basic_2.html;h=58087e46d43676ec01d4581d3575a3d058393fa3;hb=7e2f8faa727b72aeebc6eb5a49ca843dcb50dfe0;hp=1110c7060fedd03cc8aa666ddd05205669df984d;hpb=2b58d92062882492dd024a1196b6f8b788ffe5c6;p=helm.git
diff --git a/helm/www/lambda_delta/ld_basic_2.html b/helm/www/lambda_delta/ld_basic_2.html
index 1110c7060..58087e46d 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 |
|
|
|
| native typing |
| nty |
|
|
|
| conversion | context-sensitive | cpcs |
|
|
|
| computation | strongly normalizing | csn |
|
|
|
| context-sensitive | cprs |
|
|
|
| reduction | context-sensitive | lcpr |
|
|
|
|
| cpr | cpr_lift | cpr_tpss | cpr_cpr |
| context-free | ltpr | ltpr_drop |
|
|
|
| tpr | tpr_lift | tpr_tpss | tpr_tpr |
| static typing | atomic arity ass. | aaa | aaa_lift | aaa_aaa |
|
| static type ass. | sty | sty_lift | sty_sty |
|
| unfold | partial | ltpss | ltpss_drop | ltpss_tps | ltpss_ltpss |
|
| tpss | tpss_lift | tpss_tpss | tpss_ltps |
| substitution | parallel | ltps | ltps_drop | ltps_tps | ltps_ltps |
|
| tps | tps_lift | tps_tps |
|
| local env. dropping | drop | drop_drop |
|
|
| term relocation | lift | lift_lift |
|
|
| grammar | local env. equivalence | leq | leq_leq |
|
|
| 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 |
|
|
|
| native typing |
| nty |
|
|
|
| conversion | context-sensitive | cpcs |
|
|
|
| computation | strongly normalizing | csn |
|
|
|
| context-sensitive | cprs |
|
|
|
| reduction | context-sensitive | lcpr |
|
|
|
|
| cpr | cpr_lift | cpr_tpss | cpr_cpr |
| context-free | ltpr | ltpr_drop |
|
|
|
| tpr | tpr_lift | tpr_tpss | tpr_tpr |
| static typing | atomic arity ass. | aaa | aaa_lift | aaa_aaa |
|
| static type ass. | sty | sty_lift | sty_sty |
|
| unfold | partial | ltpss | ltpss_drop | ltpss_tps | ltpss_ltpss |
|
| tpss | tpss_lift | tpss_tpss | tpss_ltps |
| substitution | parallel | ltps | ltps_drop | ltps_tps | ltps_ltps |
|
| tps | tps_lift | tps_tps |
|
| local env. dropping | drop | drop_drop |
|
|
| 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.
![[lambda_delta home]](http://lambda-delta.info/images/crux_32.png "lambda_delta home")
![[Spacer]](http://lambda-delta.info/images/rainbow.png "lambda_delta rainbow rule")
![[Generated from XML via XSL]](http://lambda-delta.info/images/xml_xsl2.png "Generated from XML via XSL")
![[PNG used here]](http://lambda-delta.info/images/PNGnow2.png "PNG used here")
![[Viewable with any browser]](http://www.anybrowser.org/campaign/bvgraphics/abtfile.png "Viewable with any browser")