From: Ferruccio Guidi Date: Mon, 16 Jan 2012 12:06:47 +0000 (+0000) Subject: some additionsand refactoring in Basic_2 X-Git-Tag: make_still_working~1976 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c7e7b6d0e8a6d8c148832dad8122c68c969f1c7c;p=helm.git some additionsand refactoring in Basic_2 --- diff --git a/helm/www/lambda_delta/index.html b/helm/www/lambda_delta/index.html index 649743baf..9c266a31e 100644 --- a/helm/www/lambda_delta/index.html +++ b/helm/www/lambda_delta/index.html @@ -80,10 +80,10 @@ user [Butterfly] To view this site correctly, please select a font with Unicode -support.
+support. For example Lucida Sans Unicode -(it should be already installed on your system).
-To change the current font follow:
+(it should be already installed on your system). +To change the current font follow: "Tools" menu → "Internet Options" entry → "General" tab → "Fonts" button.
diff --git a/helm/www/lambda_delta/ld_basic_2.html b/helm/www/lambda_delta/ld_basic_2.html index fa7e4521e..e11f31a62 100644 --- a/helm/www/lambda_delta/ld_basic_2.html +++ b/helm/www/lambda_delta/ld_basic_2.html @@ -17,14 +17,14 @@
Logical structure of the contribution
The source files are grouped in planes and components according to the following table. - The notation for the relation or function introduced in each file + The notation for the relations or functions introduced in each file is shown in parentheses.
-
componentplanefiles


functionalreduction and type machinertmrtm_step ( ? ⇨ ? )


unfoldlift ( ↑[?,?] ? )subst ( [?←?] ? )

examples




native typing
nty


conversioncontext-sensitive conversioncpcs ( ? ⊢ ? ⬌* ? )


computationstrongly normalizing computationcsn ( ⬇* ? )csn_crcsn_aaa

context-sensitive computationcprs (? ⊢ ? ➡* ?)



support for abstract computation propertieslsubc ( ? [?] ⊑ ? )lsubc_ldroplsubc_ldrops


acpacp_cr ( ⦃?,?⦄ ϵ 〚?〛 )acp_aaa
reducibilitycontext-sensitive reductionlcpr ( ? ⊢ ➡ ? )




cpr ( ? ⊢ ? ➡ ? )cpr_liftcpr_ltprcpr_cpr

context-free normal formstwhnftnf


context-free reductionltpr ( ? ➡ ? )ltpr_ldrop



tpr ( ? ➡ ? )tpr_lifttpr_tpsstpr_tpr

context-free reducible formstrf


static typingstatic type ass.stysty_liftsty_sty

atomic arity ass.aaa ( ? ⊢ ? ÷ ? )aaa_liftaaa_aaa

parameterssh


unfoldterm inverse relocationdelift ( ? ⊢ ? [?,?] ≡ ? )delift_lift


partial unfoldltpss ( ? [?,?] ▶* ? )ltpss_ldropltpss_tpsltpss_ltpss


tpss ( ? ⊢ ? [?,?] ▶* ? )tpss_lifttpss_tpsstpss_ltps

generic local env. slicingldrops ( ⇩*[?] ? ≡ ? )ldrops_ldrops


generic term relocationlifts ( ⇧*[?] ? ≡ ? )lifts_liftslifts_vector ( ⇧*[?] ? ≡ ? )lifts_lifts_vector
substitutionparallel substitutionltps ( ? [?,?] ▶ ? )ltps_ldropltps_tpsltps_ltps


tps ( ? ⊢ ? [?,?] ▶ ? )tps_lifttps_tps

global env. slicinggdrop ( ⇩[?] ? ≡ ? )gdrop_gdrop


local env. slicingldrop ( ⇩[?,?] ? ≡ ? )ldrop_ldrop


term relocationlift ( ⇧[?,?] ? ≡ ? )lift_liftlift_vector ( ⇧[?,?] ? ≡ ? )lift_lift_vector
grammarlocal env. ref. for substitutionlsubs ( ? [?,?] ≼ ? )lsubs_lsubs


term hom.thomthom_thom


closurescl_shift ( ? @ ? )cl_weight ( #[?,?] )


internal syntaxgenv




lenvlenv_weight ( #[?] )lenv_length ( |?| )


termterm_weight ( #[?] )term_simpleterm_vector


item



external syntaxaarity


+
componentplanefiles


functionalreduction and type machinertmrtm_step ( ? ⇨ ? )


unfoldlift ( ↑[?,?] ? )subst ( [?←?] ? )

examples




native typing
nty


conversioncontext-sensitive conversioncpcs ( ? ⊢ ? ⬌* ? )


computationstrongly normalizing computationcsn ( ⬇* ? )csn_crcsn_aaa

context-sensitive computationcprs (? ⊢ ? ➡* ?)



support for abstract computation propertieslsubc ( ? [?] ⊑ ? )lsubc_ldroplsubc_ldrops


acpacp_cr ( ⦃?,?⦄ ϵ 〚?〛 )acp_aaa
reducibilitycontext-sensitive reductionlcpr ( ? ⊢ ➡ ? )




cpr ( ? ⊢ ? ➡ ? )cpr_liftcpr_ltprcpr_cpr

context-free normal formstwhnftnf


context-free reductionltpr ( ? ➡ ? )ltpr_ldrop



tpr ( ? ➡ ? )tpr_lifttpr_tpsstpr_tpr

context-free reducible formstrf


static typingstatic type ass.stysty_liftsty_sty

atomic arity ass.aaa ( ? ⊢ ? ÷ ? )aaa_liftaaa_aaa

parameterssh


unfoldterm inverse relocationdelift ( ? ⊢ ? [?,?] ≡ ? )delift_lift


partial unfoldltpss ( ? [?,?] ▶* ? )ltpss_ldropltpss_tpsltpss_ltpss


tpss ( ? ⊢ ? [?,?] ▶* ? )tpss_lifttpss_tpsstpss_ltps

generic local env. slicingldrops ( ⇩*[?] ? ≡ ? )ldrops_ldropldrops_ldrops

generic term relocationlifts_vector ( ⇧*[?] ? ≡ ? )lifts_lift_vector



lifts ( ⇧*[?] ? ≡ ? )lifts_liftlifts_lifts

support for generic relocationgr2gr2_gr2

substitutionparallel substitutionltps ( ? [?,?] ▶ ? )ltps_ldropltps_tpsltps_ltps


tps ( ? ⊢ ? [?,?] ▶ ? )tps_lifttps_tps

global env. slicinggdrop ( ⇩[?] ? ≡ ? )gdrop_gdrop


basic local env. slicingldrop ( ⇩[?,?] ? ≡ ? )ldrop_ldrop


basic term relocationlift_vector ( ⇧[?,?] ? ≡ ? )lift_lift_vector



lift ( ⇧[?,?] ? ≡ ? )lift_lift

grammarlocal env. ref. for substitutionlsubs ( ? [?,?] ≼ ? )lsubs_lsubs


term hom.thomthom_thom


closurescl_shift ( ? @ ? )cl_weight ( #[?,?] )


internal syntaxgenv




lenvlenv_weight ( #[?] )lenv_length ( |?| )


termterm_weight ( #[?] )term_simpleterm_vector


item



external syntaxaarity


Physical structure of the contribution
The source files are grouped in directories, one for each component.
-
[Spacer]

[Valid XHTML 1.1][Valid CSS level 2][Generated from XML via XSL][PNG used here][Viewable with any browser]

Last update: 2012-01-13+01:00
+
[Spacer]

[Valid XHTML 1.1][Valid CSS level 2][Generated from XML via XSL][PNG used here][Viewable with any browser]

Last update: 2012-01-16+01:00
diff --git a/helm/www/lambda_delta/web/home/ld_basic_2.ldw.xml b/helm/www/lambda_delta/web/home/ld_basic_2.ldw.xml index d38e7d73e..49d4094fe 100644 --- a/helm/www/lambda_delta/web/home/ld_basic_2.ldw.xml +++ b/helm/www/lambda_delta/web/home/ld_basic_2.ldw.xml @@ -8,7 +8,7 @@ Logical structure of the contribution The source files are grouped in planes and components according to the following table. - The notation for the relation or function introduced in each file + The notation for the relations or functions introduced in each file is shown in parentheses. 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 288b3c3a8..8d50bb96a 100644 --- a/helm/www/lambda_delta/web/home/ld_basic_2.tbl +++ b/helm/www/lambda_delta/web/home/ld_basic_2.tbl @@ -112,11 +112,16 @@ table { } ] [ { "generic local env. slicing" * } { - [ "ldrops ( ⇩*[?] ? ≡ ? )" "ldrops_ldrops" * ] + [ "ldrops ( ⇩*[?] ? ≡ ? )" "ldrops_ldrop" "ldrops_ldrops" * ] } ] - [ { "generic term relocation" * } { - [ "lifts ( ⇧*[?] ? ≡ ? )" "lifts_lifts" "lifts_vector ( ⇧*[?] ? ≡ ? )" "lifts_lifts_vector" * ] + [ { "generic term relocation" * } { + [ "lifts_vector ( ⇧*[?] ? ≡ ? )" "lifts_lift_vector" * ] + [ "lifts ( ⇧*[?] ? ≡ ? )" "lifts_lift" "lifts_lifts" * ] + } + ] + [ { "support for generic relocation" * } { + [ "gr2" "gr2_gr2" * ] } ] } @@ -132,12 +137,13 @@ table { [ "gdrop ( ⇩[?] ? ≡ ? )" "gdrop_gdrop" * ] } ] - [ { "local env. slicing" * } { + [ { "basic local env. slicing" * } { [ "ldrop ( ⇩[?,?] ? ≡ ? )" "ldrop_ldrop" * ] } ] - [ { "term relocation" * } { - [ "lift ( ⇧[?,?] ? ≡ ? )" "lift_lift" "lift_vector ( ⇧[?,?] ? ≡ ? )" "lift_lift_vector" * ] + [ { "basic term relocation" * } { + [ "lift_vector ( ⇧[?,?] ? ≡ ? )" "lift_lift_vector" * ] + [ "lift ( ⇧[?,?] ? ≡ ? )" "lift_lift" * ] } ] }