From: Ferruccio Guidi Date: Thu, 15 Mar 2012 19:03:49 +0000 (+0000) Subject: renaming completed X-Git-Tag: make_still_working~1848 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=70e6a24c9505c950714f138506f3eedb293084c5;p=helm.git renaming completed --- diff --git a/helm/www/lambda_delta/apps_2.html b/helm/www/lambda_delta/apps_2.html index 0344bee55..e6634f9aa 100644 --- a/helm/www/lambda_delta/apps_2.html +++ b/helm/www/lambda_delta/apps_2.html @@ -51,7 +51,7 @@ The notation for the relations or functions introduced in each file is shown in parentheses. -
+
componentplanefiles
MLTT1
genv_primitivejudgement
functionalreduction and type machinertmrtm_step ( ? ⇨ ? )

unfoldlift ( ↑[?,?] ? )subst ( [?←?] ? )
Physical Structure of the Specification
The source files are grouped in directories, diff --git a/helm/www/lambda_delta/basic_2.html b/helm/www/lambda_delta/basic_2.html index 65a801e7e..8d1fc3ea5 100644 --- a/helm/www/lambda_delta/basic_2.html +++ b/helm/www/lambda_delta/basic_2.html @@ -18,7 +18,7 @@
This is a summary of the "block structure" of the System's syntactic items and reductions.
-
+
domainblockleaderapplicator (with →θ)*reduction→ζ *reference *
{X | Γ ⊢ X : W}typed abstraction **Γ ⊢ λWⓐV→βno#i

typed declaration ***Γ ⊢ pλWnonono$p

native type annotation *Γ ⊢ ⓣWnonoyesno
{X | Γ ⊢ X = V}local abbreviation **Γ ⊢ δVnolocal →δyes#i

global abbreviation ***Γ ⊢ pδVnoglobal →δno$p
nosort ****Γ ⊢ ⋆knononono
* In terms only. ** In terms and local environments only. *** In global environments only. @@ -62,7 +62,7 @@ The notation for the relations or functions introduced in each file is shown in parentheses.
-
+
componentplanefiles





examples







native typing
nty





equivalencecontext-sensitive equivalencecpcs ( ? ⊢ ? ⬌* ? )





conversioncontext-sensitive conversioncpc ( ? ⊢ ? ⬌ ? )cpc_cpc




computationstrongly normalizing computationcsn_vector ( ⬇* ? )csn_cpr_vectorcsn_tstc_vectorcsn_aaa




csn ( ⬇* ? )csn_liftcsn_cprcsn_cprs ( ⬇** ? )csn_lcpr


context-sensitive computationlcprs ( ? ⊢ ➡* ? )lcprs_cprslcprs_lcprs





cprs (? ⊢ ? ➡* ?)cprs_liftcprs_lcprcprs_cprscprs_lcprscprs_tstccprs_tstc_vector

local env. ref. for abstract candidates of reducibilitylsubc ( ? [?] ⊑ ? )lsubc_ldroplsubc_ldropslsubc_lsuba



support for abstract computation propertiesacpacp_cr ( ⦃?,?⦄ ϵ 〚?〛 )acp_aaa



reducibilitycontext-sensitive normal formscnf ( ? ⊢ 𝐍[?] )cnf_lift





context-sensitive reductionlcpr ( ? ⊢ ➡ ? )lcpr_cpr






cpr ( ? ⊢ ? ➡ ? )cpr_liftcpr_ltpsscpr_ltprcpr_cpr


context-free normal formstwhnf ( 𝐖𝐇𝐍[?] )tnf ( 𝐍[?] )tnf_tif




context-free reductionltpr ( ? ➡ ? )ltpr_ldropltpr_tps





tpr ( ? ➡ ? )tpr_lifttpr_tpsstpr_tpr



context-free reducible formstrf ( 𝐑[?] )tif ( 𝐈[?] )




static typingstatic type assignmentstysty_liftsty_sty




local env. ref. for atomic arity assignmentlsuba ( ? ÷⊑ ? )lsuba_ldroplsuba_aaalsuba_lsuba



atomic arity assignmentaaa ( ? ⊢ ? ÷ ? )aaa_liftaaa_liftsaaa_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 relocationgr2 ( @ [ ? ] ? ≡ ? )gr2_plus ( ? + ? )gr2_minus ( ? ▭ ? ≡ ? )gr2_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





same head term formtshf ( ? ≈ ? )tshf_tshf





same top term constructortstc ( ? ≃ ? )tstc_tstctstc_vector




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





internal syntaxgenv







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





termterm_weight ( #[?] )term_simple ( 𝐒[?] )term_vector




item






external syntaxaarity





Physical Structure of the Specification
The source files are grouped in directories, diff --git a/helm/www/lambda_delta/web/home/apps_2_src.tbl b/helm/www/lambda_delta/web/home/apps_2_src.tbl index df8a5602a..d5508e3d6 100644 --- a/helm/www/lambda_delta/web/home/apps_2_src.tbl +++ b/helm/www/lambda_delta/web/home/apps_2_src.tbl @@ -1,4 +1,4 @@ -name "ld_apps_2_src" +name "apps_2_src" table { class "grey" diff --git a/helm/www/lambda_delta/web/home/basic_2_blk.tbl b/helm/www/lambda_delta/web/home/basic_2_blk.tbl index 8e3ada607..01a4d1c2a 100644 --- a/helm/www/lambda_delta/web/home/basic_2_blk.tbl +++ b/helm/www/lambda_delta/web/home/basic_2_blk.tbl @@ -1,4 +1,4 @@ -name "ld_basic_2_blk" +name "basic_2_blk" table { class "grey" [ { "domain" * } { diff --git a/helm/www/lambda_delta/web/home/basic_2_src.tbl b/helm/www/lambda_delta/web/home/basic_2_src.tbl index 4dfeb8017..7fd4437a1 100644 --- a/helm/www/lambda_delta/web/home/basic_2_src.tbl +++ b/helm/www/lambda_delta/web/home/basic_2_src.tbl @@ -1,4 +1,4 @@ -name "ld_basic_2_src" +name "basic_2_src" table { class "grey"