X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=3511fbfb0705ac2586194136823161960b181683;hb=2aa295aa37f8fb274f7b640f7627078d9435cefa;hp=c2b832a96db65304d87757316a94ca8e0fd1b876;hpb=03e9a07b37a7e372f8ee88071b05bd3f49a0b368;p=helm.git diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index c2b832a96..3511fbfb0 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -1,88 +1,1305 @@ - + - - - - - - lambdadelta version 2 - - - - + + + + + + \lambda\delta version 2 + + + + -
[lambdadelta home]
cic:/matita/lambdadelta/basic_2/ (λδ version 2)
[Spacer]
-
System's Syntax and Behavior
-
This is a summary of the "block structure" - of the System's syntactic items and reductions. -
-
domainblockleaderapplicator (with →θ)*reduction→ζ *reference *
{X | Γ ⊢ X : W}local typed abstraction *Γ ⊢ +λWⓐV→βno#i

local typed declaration **Γ ⊢ -λWⓐV→βno#i

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

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

local definition **Γ ⊢ -δVnolocal →δno#i

global definition ***Γ ⊢ pδVnoglobal →δno$p
nosort ****Γ ⊢ ⋆knononono
-
* In terms only. - ** In terms and local environments only. - *** In global environments only. - **** Sort level k in terms only. -
- -
Summary of the Specification
-
Here is a numerical acount of the specification's contents + +
+ + [lambdadelta home] + +
+
cic:/matita/lambdadelta/basic_2/ (λδ version 2)
+
+ [Spacer] +
+ + +
Summary of the Specification
+
Here is a numerical acount of the specification's contents and its timeline. + Nodes are counted according to the "intrinsinc complexity measure" + [F. Guidi: "Procedural Representation of CIC Proof Terms" + Journal of Automated Reasoning 44(1-2), Springer (February 2010), + pp. 53-78].
-
- -
Logical Structure of the Specification
-
The source files are grouped in planes and components +
Logical Structure of the Specification
+
The source files are grouped in planes and components according to the following table. - A notation file covering the whole specification is provided. - The notation for the relations or functions introduced in each file - is shown in parentheses (? are placeholders). + Notation files covering the whole specification are provided. + The notation for the relations or functions introduced in each file + is shown in parentheses (? are placeholders).
-
componentplanefiles



dynamic typingstratified native validitysnv ( ⦃?,?⦄ ⊩ ? :[?] )snv_lift snv_aaa snv_ssta snv_ltpr


equivalencefocalized equivalencelfpcs ( ⦃?⦄ ⬌* ⦃?⦄ )lfpcs_aaa lfpcs_lfprs lfpcs_lfpcs




fpcs ( ⦃?,?⦄ ⬌* ⦃?,?⦄ )fpcs_aaa fpcs_cpcs fpcs_fprs fpcs_fpcs



local env. ref. for context-sensitive equivalencelsubse ( ? ⊢•⊑[?] ? )lsubse_ldrop lsubse_ssta lsubse_cpcs



context-sensitive equivalencecpcs ( ? ⊢ ? ⬌* ? )cpcs_ltpss cpcs_delift cpcs_aaa cpcs_ltpr cpcs_cprs cpcs_cpcs


conversionfocalized conversionlfpc ( ⦃?⦄ ⬌ ⦃?⦄ )lfpc_lfpc




fpc ( ⦃?,?⦄ ⬌ ⦃?,?⦄ )fpc_fpc



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


computationextended computationxprs ( ⦃?,?⦄ ⊢ ? •➡*[?] ? )xprs_lift xprs_aaa xpr_lsubss xprs_cprs xprs_xprs



weakly normalizing computationcpe ( ? ⊢ ➡* 𝐍⦃?⦄ )cpe_cpe



strongly normalizing computationcsn_vector ( ? ⊢ ⬊* ? )csn_cpr_vector csn_tstc_vector csn_aaa




csn ( ? ⊢ ⬊* ? )csn_alt ( ? ⊢ ⬊⬊* ? )csn_lift csn_cpr csn_lfpr


focalized computationlfprs ( ⦃?⦄ ➡* ⦃?⦄ )lfprs_aaa lfprs_ltprs lfprs_cprs lfprs_fprs lfprs_lfprs




fprs ( ⦃?,?⦄ ➡* ⦃?,?⦄ )fprs_aaa fprs_fprs



context-sensitive computationcprs (? ⊢ ? ➡* ?)cprs_lift cprs_delift cprs_aaa cprs_ltpr cprs_lfpr cprs_cprs cprs_lfprs cprs_tstc cprs_tstc_vector



context-free computationltprs ( ? ➡* ? )ltprs_alt ( ? ➡➡* ? )ltprs_ldrop ltprs_ltprs



tprs ( ? ➡* ?)tprs_lift tprs_tprs



local env. ref. for abstract candidates of reducibilitylsubc ( ? ⊑[?] ? )lsubc_ldrop lsubc_ldrops lsubc_lsuba



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

reducibilityextended reductionxpr ( ⦃?,?⦄ ⊢ ? •➡[?] ? )xpr_lift xpr_aaa xpr_lsubss



context-sensitive focalized reductioncfpr ( ? ⊢ ⦃?,?⦄ ➡ ⦃?,?⦄ )cnfpr_ltpss cfpr_aaa cfpr_cpr cfpr_cfpr



context-free focalized reductionlfpr ( ⦃?⦄ ➡ ⦃?⦄ )lfpr_alt ( ⦃?⦄ ➡➡ ⦃?⦄ )lfpr_aaa lfpr_cpr lfpr_fpr lfpr_lfpr



fpr ( ⦃?,?⦄ ➡ ⦃?,?⦄ )fpr_cpr fpr_fpr



context-sensitive normal formscnf ( ? ⊢ 𝐍⦃?⦄ )cnf_lift cnf_cif



context-sensitive reductioncpr ( ? ⊢ ? ➡ ? )cpr_lift cpr_tpss cpr_ltpss cpr_delift cpr_aaa cpr_ltpr cpr_cpr



context-sensitive reducible formscrf ( ? ⊢ 𝐑⦃?⦄ )crf_appendcif ( ? ⊢ 𝐈⦃?⦄ )cif_append

context-free normal formsthnf ( 𝐇𝐍⦃?⦄ )




context-free reductionltpr ( ? ➡ ? )ltpr_ldrop ltpr_tps ltpr_ltpss_dx ltpr_ltpss_sn ltpr_aaa ltpr_ltpr




tpr ( ? ➡ ? )tpr_lift tpr_tps tpr_tpss tpr_delift tpr_tpr


unwind



static typinglocal env. ref. for stratified static type assignmentlsubss ( ? •⊑[?] ? )lsubss_ldrop lsubss_ssta lsubss_lsubss



stratified static type assignmentssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )ssta_lift ssta_ltpss_dx ssta_ltpss_sn ssta_aaa ssta_ssta



local env. ref. for atomic arity assignmentlsuba ( ? ⁝⊑ ? )lsuba_ldrop lsuba_aaa lsuba_lsuba



atomic arity assignmentaaa ( ? ⊢ ? ⁝ ? )aaa_lift aaa_lifts aaa_ltpss_dx aaa_ltpss_sn aaa_aaa



parametersshsd


unfoldbasic local env. thinningthin ( ? ▼*[?,?] ≡ ? )thin_ldrop thin_delift



inverse basic term relocationdelift ( ? ⊢ ? ▼*[?,?] ≡ ? )delift_alt ( ? ⊢ ? ▼▼*[?,?] ≡ ? )delift_lift delift_tpss delift_ltpss delift_delift


partial unfoldltpss_sn ( ? ⊢ ▶*[?,?] ? )ltpss_sn_alt ( ? ⊢ ▶▶*[?,?] ? )ltpss_sn_ldrop ltpss_sn_tps ltpss_sn_tpss ltpss_sn_ltpss_sn



ltpss_dx ( ? ▶*[?,?] ? )ltpss_dx_ldrop ltpss_dx_tps ltpss_dx_tpss ltpss_dx_ltpss_dx




tpss ( ? ⊢ ? ▶*[?,?] ? )tpss_alt ( ? ⊢ ? ▶▶*[?,?] ? )tpss_lifttpss_tpss

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



iterated restricted structural predecessor for closuresfrsups ( ⦃?,?⦄ ⧁* ⦃?,?⦄ )frsups_frsups




frsupp ( ⦃?,?⦄ ⧁+ ⦃?,?⦄ )frsupp_frsupp



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




lifts ( ⇧*[?] ? ≡ ? )lifts_lift lifts_lifts



support for generic relocationgr2 ( @⦃?,?⦄ ≡ ? )gr2_plus ( ? + ? )gr2_minus ( ? ▭ ? ≡ ? )gr2_gr2
substitutionparallel substitutiontps ( ? ⊢ ? ▶[?,?] ? )tps_lift tps_tps



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



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



local env. ref. for substitutionlsubs ( ? ≼[?,?] ? )(lsubs_lsubs)lsubs_sfr ( ≽[?,?] ? )


restricted structural predecessor for closuresfrsup ( ⦃?,?⦄ ⧁ ⦃?,?⦄ )




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




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


grammarsame head term formtshf ( ? ≈ ? )(tshf_tshf)



same top term constructortstc ( ? ≃ ? )tstc_tstc tstc_vector



closurescl_shift ( ? @@ ? )cl_weight ( ♯{?,?} )



internal syntaxgenv





lenvlenv_weight ( ♯{?} )lenv_length ( |?| )lenv_append ( ? @@ ? )lenv_px lenv_px_bi


termterm_weight ( ♯{?} )term_simple ( 𝐒⦃?⦄ )term_vector


item




external syntaxaarity



+
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
componentplanefiles +
+ 		+
+ 		+
+
examplesterms with special featuresex_cpr_omega +
+ 		+
+ 		+
+
+ + + +
+ 		+
+ 		+
+
dynamic typinglocal env. ref. for stratified native validitylsubsv ( ? ⊢ ? ¡⫃[?,?] ? )lsubsv_lsuba lsubsv_lsubd lsubsv_lstas lsubsv_cpds lsubsv_cpcs lsubsv_snv +
+ 		+
+
+
+ 		stratified native validitysnv ( ⦃?,?⦄ ⊢ ? ¡[?,?] )snv_lift snv_aaa snv_da_lpr snv_lstas snv_lstas_lpr snv_lpr snv_cpcs snv_preserve +
+ 		+
+
equivalencedecomposed extended equivalencecpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?] ? )cpes_cpds +
+ 		+
+
+
+ 		context-sensitive equivalencecpcs ( ⦃?,?⦄ ⊢ ? ⬌* ? )cpcs_aaa cpcs_cprs cpcs_cpcs +
+ 		+
+
conversioncontext-sensitive conversioncpc ( ⦃?,?⦄ ⊢ ? ⬌ ? )cpc_cpc +
+ 		+
+
computationevaluation for context-sensitive extended reductioncpxe ( ⦃?,?⦄ ⊢ ➡*[?,?] 𝐍⦃?⦄ ) +
+ 		+
+ 		+
+
+
+ 		evaluation for context-sensitive reductioncpre ( ⦃?,?⦄ ⊢ ➡* 𝐍⦃?⦄ )cpre_cpre +
+ 		+
+
+
+ 		strongly normalizing "big tree" computationfsb ( ⦃?,?⦄ ⊢ ⦥[?,?] ? )fsb_alt ( ⦃?,?⦄ ⊢ ⦥⦥[?,?] ? )fsb_aaa fsb_csx +
+
+
+ 		strongly normalizing extended computationlcosx ( ? ⊢ ~⬊*[?,?,?] ? )lcosx_cpx +
+ 		+
+
+
+ 		+
+ 		lsx ( ? ⊢ ⬊*[?,?,?,?] ? )lsx_alt ( ? ⊢ ⬊⬊*[?,?,?,?] ? )lsx_drop lsx_lpx lsx_lpxs llsx_csx +
+
+
+ 		+
+ 		csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )csx_tstc_vector csx_aaa +
+ 		+
+
+
+ 		+
+ 		csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )csx_lift csx_lleq csx_lpx csx_lpxs csx_fpbs +
+
+
+ 		"big tree" parallel computationfpbg ( ⦃?,?,?⦄ >≡[?,?] ⦃?,?,?⦄ )fpbg_lift fpbg_fleq fpbg_fpbg +
+ 		+
+
+
+ 		+
+ 		fpbc ( ⦃?,?,?⦄ ≻≡[?,?] ⦃?,?,?⦄ )fpbc_fleq fpbc_fpbs +
+ 		+
+
+
+ 		+
+ 		fpbu ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )fpbu_lift fpbu_lleqfpbu_fleq +
+
+
+ 		+
+ 		fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )fpbs_lift fpbs_fleq fpbs_aaa fpbs_fpbs fpbs_ext +
+
+
+ 		decomposed extended computationcpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?] ? )cpds_lift cpds_aaa cpds_cpds +
+ 		+
+
+
+ 		context-sensitive extended computationlpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )lpxs_drop lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs +
+ 		+
+
+
+ 		+
+ 		cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )cpxs_tstc cpxs_tstc_vector cpxs_leq cpxs_lift cpxs_lleq cpxs_aaa cpxs_cpxs +
+ 		+
+
+
+ 		context-sensitive computationlprs ( ⦃?,?⦄ ⊢ ➡* ? )lprs_drop lprs_cprs lprs_lprs +
+ 		+
+
+
+ 		+
+ 		cprs ( ⦃?,?⦄ ⊢ ? ➡* ?)cprs_lift cprs_cprs +
+ 		+
+
+
+ 		local env. ref. for abstract candidates of reducibilitylsubc ( ? ⊢ ? ⫃[?] ? )lsubc_drop lsubc_drops lsubc_lsuba +
+ 		+
+
+
+ 		support for abstract computation propertiesacpacp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )acp_aaa +
+
reduction"big tree" parallel reductionfpb ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )fpb_lift fpb_aaa +
+ 		+
+
+
+ 		normal forms for context-sensitive extended reductioncnx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐍⦃?⦄ )cnx_lift cnx_crx cnx_cix +
+ 		+
+
+
+ 		context-sensitive extended reductionlpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )lpx_drop lpx_freeslpx_lleq lpx_aaa +
+
+
+ 		+
+ 		cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )cpx_leq cpx_lift cpx_llpx_sn cpx_lleq cpx_cix +
+ 		+
+
+
+ 		irreducible forms for context-sensitive extended reductioncix ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐈⦃?⦄ )cix_lift +
+ 		+
+
+
+ 		reducible forms for context-sensitive extended reductioncrx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐑⦃?⦄ )crx_lift +
+ 		+
+
+
+ 		normal forms for context-sensitive reductioncnr ( ⦃?,?⦄ ⊢ ➡ 𝐍⦃?⦄ )cnr_lift cnr_crr cnr_cir +
+ 		+
+
+
+ 		context-sensitive reductionlpr ( ⦃?,?⦄ ⊢ ➡ ? )lpr_drop lpr_lpr +
+ 		+
+
+
+ 		+
+ 		cpr ( ⦃?,?⦄ ⊢ ? ➡ ? )cpr_lift cpr_llpx_sn cpr_cir +
+ 		+
+
+
+ 		irreducible forms for context-sensitive reductioncir ( ⦃?,?⦄ ⊢ ➡ 𝐈⦃?⦄ )cir_lift +
+ 		+
+
+
+ 		reducible forms for context-sensitive reductioncrr ( ⦃?,?⦄ ⊢ ➡ 𝐑⦃?⦄ )crr_lift +
+ 		+
+
unfoldunfoldunfold ( ⦃?,?⦄ ⊢ ? ⧫* ? ) +
+ 		+
+ 		+
+
+
+ 		iterated static type assignmentlstas ( ⦃?,?⦄ ⊢ ? •*[?,?] ? )lstas_alt ( ⦃?,?⦄ ⊢ ? ••*[?,?] ? )lstas_lift lstas_aaa lstas_da lstas_lstas +
+
static typinglocal env. ref. for degree assignmentlsubd ( ? ⊢ ? ▪⫃ ? )lsubd_da lsubd_lsubd +
+ 		+
+
+
+ 		degree assignmentda ( ⦃?,?⦄ ⊢ ? ▪[?,?] ? )da_lift da_aaa da_sta da_da +
+ 		+
+
+
+ 		static type assignmentsta ( ⦃?,?⦄ ⊢ ? •[?] ? )sta_lift sta_lpx_sn sta_aaa sta_sta +
+ 		+
+
+
+ 		parametersshsd +
+ 		+
+
+
+ 		local env. ref. for atomic arity assignmentlsuba ( ? ⊢ ? ⁝⫃ ? )lsuba_aaa lsuba_lsuba +
+ 		+
+
+
+ 		atomic arity assignmentaaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )aaa_lift aaa_lifts aaa_fqus aaa_lleq aaa_aaa +
+ 		+
+
+
+ 		restricted local env. ref.lsubr ( ? ⫃ ? )lsubr_lsubr +
+ 		+
+
multiple substitutionlazy equivalencefleq ( ⦃?,?,?⦄ ≡[?] ⦃?,?,?⦄ )fleq_fleq +
+ 		+
+
+
+ 		+
+ 		lleq ( ? ≡[?,?] ? )lleq_alt lleq_alt_rec lleq_leq lleq_drop lleq_fqus lleq_llor lleq_lleq +
+ 		+
+
+
+ 		lazy pointwise extension of a relationllpx_snllpx_sn_alt llpx_sn_alt_rec llpx_sn_tc llpx_sn_leq llpx_sn_drop llpx_sn_lpx_sn llpx_sn_frees llpx_sn_llor +
+ 		+
+
+
+ 		pointwise union for local environmentsllor ( ? ⩖[?,?] ? ≡ ? )llor_alt llor_drop +
+ 		+
+
+
+ 		context-sensitive exclusion from free variablesfrees ( ? ⊢ ? ϵ 𝐅*[?]⦃?⦄ )frees_append frees_leq frees_lift +
+ 		+
+
+
+ 		contxt-sensitive extended multiple substitutioncpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? )cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? )cpys_lift cpys_cpys +
+
+
+ 		iterated structural successor for closuresfqus ( ⦃?,?,?⦄ ⊐* ⦃?,?,?⦄ )fqus_alt fqus_fqus +
+ 		+
+
+
+ 		+
+ 		fqup ( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ )fqup_fqup +
+ 		+
+
+
+ 		iterated local env. slicingdrops ( ⇩*[?,?] ? ≡ ? )drops_drop drops_drops +
+ 		+
+
+
+ 		generic term relocationlifts_vector ( ⇧*[?] ? ≡ ? )lifts_lift_vector +
+ 		+
+
+
+ 		+
+ 		lifts ( ⇧*[?] ? ≡ ? )lifts_lift lifts_lifts +
+ 		+
+
+
+ 		support for generic relocationgr2 ( @⦃?,?⦄ ≡ ? )gr2_plus ( ? + ? )gr2_minus ( ? ▭ ? ≡ ? )gr2_gr2
substitutionstructural successor for closuresfquq ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ )fquq_alt ( ⦃?,?,?⦄ ⊐⊐⸮ ⦃?,?,?⦄ ) +
+ 		+
+
+
+ 		+
+ 		fqu ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ ) +
+ 		+
+ 		+
+
+
+ 		global env. slicinggget ( ⇩[?] ? ≡ ? )gget_gget +
+ 		+
+
+
+ 		contxt-sensitive extended ordinary substitutioncpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? )cpy_lift cpy_nlift cpy_cpy +
+ 		+
+
+
+ 		local env. ref. for extended substitutionlsuby ( ? ⊑×[?,?] ? )lsuby_lsuby +
+ 		+
+
+
+ 		pointwise extension of a relationlpx_snlpx_sn_alt lpx_sn_tc lpx_sn_drop lpx_sn_lpx_sn +
+ 		+
+
+
+ 		basic local env. slicingdrop ( ⇩[?,?,?] ? ≡ ? )drop_append drop_leq drop_drop +
+ 		+
+
+
+ 		basic term relocationlift_vector ( ⇧[?,?] ? ≡ ? )lift_lift_vector +
+ 		+
+
+
+ 		+
+ 		lift ( ⇧[?,?] ? ≡ ? )lift_neq lift_lift +
+ 		+
+
grammarequivalence for local environmentsleq ( ? ⩬[?,?] ? )leq_leq +
+ 		+
+
+
+ 		same top term constructortstc ( ? ≂ ? )tstc_tstc tstc_vector +
+ 		+
+
+
+ 		closurescl_weight ( ♯{?,?,?} )cl_restricted_weight ( ♯{?,?} ) +
+ 		+
+
+
+ 		internal syntaxgenv +
+ 		+
+ 		+
+
+
+ 		+
+ 		lenvlenv_weight ( ♯{?} )lenv_length ( |?| )lenv_append ( ? @@ ? )
+
+ 		+
+ 		termterm_weight ( ♯{?} )term_simple ( 𝐒⦃?⦄ )term_vector
+
+ 		+
+ 		item +
+ 		+
+ 		+
+
+
+ 		external syntaxaarity +
+ 		+
+ 		+
+
+
-
Physical Structure of the Specification
-
The source files are grouped in directories, +
Physical Structure of the Specification
+
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: 2013-02-07T20:49:53+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: Sun, 06 Jul 2014 20:28:30 +0200