From: Ferruccio Guidi Date: Fri, 13 Jan 2012 15:44:30 +0000 (+0000) Subject: more file names added to Basic_2 X-Git-Tag: make_still_working~1977 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2aea8f344b5bb1cd15b39203026fa70bee25a408;p=helm.git more file names added to Basic_2 --- diff --git a/helm/www/lambda_delta/Makefile b/helm/www/lambda_delta/Makefile index 173c4d78c..ae43f1cf4 100644 --- a/helm/www/lambda_delta/Makefile +++ b/helm/www/lambda_delta/Makefile @@ -3,7 +3,7 @@ H=@ TAGS = lint-xml index lddl install-xml \ test-html html install-html \ install-jed install-bib \ - up + www up LDDLURL = http://lambda-delta.info/static/lddl @@ -14,6 +14,7 @@ XMLDIR = xml HTMLDIR = $(HOME)/public_html/lddl JEDDIR = $(HOME)/mps/jed BIBDIR = $(HOME)/texmf/bibtex/bib +XHTBLDIR = bin/xhtbl REMOTE = helm.cs.unibo.it RDIR = /projects/helm/public_html/lambda_delta @@ -75,6 +76,10 @@ install-bib: $(BIB:%=$(BIBDIR)/%) $(H)scp $< $(DOWNDIR) $(H)scp $< $(DOWNDIR)/$(BIB:%.bib=%.txt) +www: + @echo " UPDATE HOME PAGES" + $(H)$(MAKE) --no-print-directory -C $(XHTBLDIR) test + up: @echo " UPDATE $(REMOTE):$(RDIR)" $(H)ssh $(REMOTE) "svn up $(RDIR)" diff --git a/helm/www/lambda_delta/ld_basic_2.html b/helm/www/lambda_delta/ld_basic_2.html index eaa539756..fa7e4521e 100644 --- a/helm/www/lambda_delta/ld_basic_2.html +++ b/helm/www/lambda_delta/ld_basic_2.html @@ -20,11 +20,11 @@ The notation for the relation or function 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 relocationlifts ( ⇧*[?] ? ≡ ? )lifts_liftslifts_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
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_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


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-08+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-13+01:00
diff --git a/helm/www/lambda_delta/news.html b/helm/www/lambda_delta/news.html index 6f8d840a1..e3d13c5ee 100644 --- a/helm/www/lambda_delta/news.html +++ b/helm/www/lambda_delta/news.html @@ -129,7 +129,7 @@ pages of the specification of λδ in Matita 0.5 are online.