X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fwww%2Flambdadelta%2Fbasic_2.html;h=68f455388549923329a0a6a8a2c8cb231e4dc59b;hb=bb1a03359dfaea6031592d28b9bfb15d797c44e5;hp=71e25ea8f394b1559e18e5d251bdd3db67c25438;hpb=6aec17030b294a256e69c32eb7bf638fefec9f85;p=helm.git diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index 71e25ea8f..68f455388 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -25,7 +25,7 @@ -
Summary of the Specification
+
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" @@ -37,54 +37,56 @@ - - - + + - - - - - - - - - - - + + + + + + + - - - - - - - + + + + + + + - - - - - - - + + + + + + +
categoryobjects + categoryobjects
+
+
+
+
sizesfiles363characters652617nodes1820917sizesfiles359characters429712nodes1856521
propositionstheorems122lemmas1295total1417propositionstheorems127lemmas1273total1400
conceptsdeclared55defined81total136conceptsdeclared54defined83total137
+ +
Stage "B"
+ +
Stage "A": "Weakening the Applicability Condition"
+ -
Logical Structure of the Specification
+
Logical Structure of the Specification
The source files are grouped in planes and components according to the following table. Notation files covering the whole specification are provided. @@ -219,1036 +230,1058 @@ - - - - + + + - - - - - - - + + + + - - - - - - - - - - - - + + + + - - + + + - - - - - - - - - - - - - - - - - + + - - + + + + + + + - - - - - + + + - - + + + + - - - - - - + + + - - - - - - - + + + - - - - - - - - - - + + + + - - + + + - - - - - - - - - - + + + - - - - - + + - - - - - - - + + + - - + + + - - - - - + - - - - + + - - + - - - - + + - - - - - - + + + - + + + + + + + - - - - - + + + - - - - - - + + - - - - - - + + + - - - - - - - - - - - - - - + + - - - - - - + + + - - - - - - - + + + + - + + + + + - + + - - - + + + - - - - - - + + + - - - - - - - + + + - - - - - + + + - - - - - - + + + - - - - - - + + + - - - - - - + + + - - + - - - - + + - - - - - - + + + - - - - - - - + + + + - - - - - + + + + - - - - - - + + + - - - - - - + + + + - - - - - - + + + - - - - - - + + + - - - - - - + + + - - - - - - + + + - - - - - - + + + - - - - - - + + + + - - - - - - + + - - - - - - + + + - - - - - - + + + - - - - - - + + + - - - - - - - + + + + - - - - - + + + - - - - - - + + - - - - - - + + + - - - - - - + + + - - - - - - + + - - - - - - - + + + + + - - - - - + + + + - - - - - + - - - - - - - + + + - - - - - - + + + - - - - - - + + + - - - - - - + + + - - - - - - + + + - - - - - - + + + - - - - - - + + - - - - - - + + + + - - - - - - + + + - - - - - - + + + - - - - - + + - - - - - - - - + + + + - - - - - - + + + + - - - - + - - - - - - + + - - @@ -1256,7 +1289,7 @@
componentplanefiles + componentplanefiles
+
+
dynamic typinglocal env. ref. for stratified native validitylsubsv ( ? ⊢ ? ¡⫃[?,?] ? )lsubsv_lsuba lsubsv_lsubd lsubsv_lstas lsubsv_cpds lsubsv_cpcs lsubsv_snv + examplesterms with special featuresex_sta_ldecex_cpr_omega
+
+ + + +
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 + dynamic typinglocal env. ref. for stratified native validitylsubsv ( ? ⊢ ? ⫃¡[?,?] ? )lsubsv_lsuba lsubsv_lsubd lsubsv_lstas lsubsv_scpds lsubsv_cpcs lsubsv_snv
+
+ +
+ 		stratified native validityshnv ( ⦃?,?⦄ ⊢ ? ¡[?,?,?] )
context-sensitive equivalencecpcs ( ⦃?,?⦄ ⊢ ? ⬌* ? )cpcs_aaa cpcs_cprs cpcs_cpcs +
+
conversioncontext-sensitive conversioncpc ( ⦃?,?⦄ ⊢ ? ⬌ ? )cpc_cpc +
+
computationevaluation for context-sensitive extended reductioncpxe ( ⦃?,?⦄ ⊢ ➡*[?,?] 𝐍⦃?⦄ ) + snv ( ⦃?,?⦄ ⊢ ? ¡[?,?] )snv_lift snv_aaa snv_da_lpr snv_lstas snv_lstas_lpr snv_lpr snv_scpes snv_preserve
+
+
equivalencedecomposed extended equivalencescpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?,?,?] ? )scpes_aaa scpes_cpcs scpes_scpes +
+
+
evaluation for context-sensitive reductioncpre ( ⦃?,?⦄ ⊢ ➡* 𝐍⦃?⦄ )cpre_cpre + context-sensitive equivalencecpcs ( ⦃?,?⦄ ⊢ ? ⬌* ? )cpcs_aaa cpcs_cprs cpcs_cpcs
+
+ conversioncontext-sensitive conversioncpc ( ⦃?,?⦄ ⊢ ? ⬌ ? )cpc_cpc
strongly normalizing "big tree" computationfsb ( ⦃?,?⦄ ⊢ ⦥[?,?] ? )fsb_alt ( ⦃?,?⦄ ⊢ ⦥⦥[?,?] ? )fsb_aaa fsb_csx +
+ computationevaluation for context-sensitive extended reductioncpxe ( ⦃?,?⦄ ⊢ ➡*[?,?] 𝐍⦃?⦄ )
strongly normalizing extended computationlcosx ( ? ⊢ ~⬊*[?,?,?] ? )lcosx_cpx +
+
+
+ evaluation for context-sensitive reductioncpre ( ⦃?,?⦄ ⊢ ➡* 𝐍⦃?⦄ )cpre_cpre
lsx ( ? ⊢ ⬊*[?,?,?,?] ? )lsx_alt ( ? ⊢ ⬊⬊*[?,?,?,?] ? )lsx_ldrop lsx_lpx lsx_lpxs llsx_csx +
-
- 		+
csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )csx_tstc_vector csx_aaa -
- 		+ strongly normalizing "big tree" computationfsb ( ⦃?,?⦄ ⊢ ⦥[?,?] ? )fsb_alt ( ⦃?,?⦄ ⊢ ⦥⦥[?,?] ? )fsb_aaa fsb_csx
+
+ strongly normalizing extended computationlcosx ( ? ⊢ ~⬊*[?,?,?] ? )lcosx_cpx
csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )csx_lift csx_lleq csx_lpx csx_lpxs csx_fpbs +
+
"big tree" parallel computationfpbg ( ⦃?,?,?⦄ >≡[?,?] ⦃?,?,?⦄ )fpbg_lift fpbg_fleq fpbg_fpbg +
+ lsx ( ? ⊢ ⬊*[?,?,?,?] ? )lsx_alt ( ? ⊢ ⬊⬊*[?,?,?,?] ? )lsx_drop lsx_lpx lsx_lpxs llsx_csx
+
+
fpbc ( ⦃?,?,?⦄ ≻≡[?,?] ⦃?,?,?⦄ )fpbc_fleq fpbc_fpbs + csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )csx_tsts_vector csx_aaa
+
+
+
fpbu ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )fpbu_lift fpbu_lleqfpbu_fleq + csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )csx_lift csx_lleq csx_lpx csx_lpxs csx_fpbs
+
+ "big tree" parallel computationfpbg ( ⦃?,?,?⦄ >≡[?,?] ⦃?,?,?⦄ )fpbg_lift fpbg_fleq fpbg_fpbg
fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )fpbs_lift fpbs_fleq fpbs_aaa fpbs_fpbs fpbs_ext +
+ +
+
decomposed extended computationcpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?] ? )cpds_lift cpds_aaa cpds_cpds + fpbc ( ⦃?,?,?⦄ ≻≡[?,?] ⦃?,?,?⦄ )fpbc_fleq fpbc_fpbs
+
+ +
+
context-sensitive extended computationlpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )lpxs_ldrop lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs + fpbu ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )fpbu_lift fpbu_lleq fpbu_fleq
+
+
+
cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )cpxs_tstc cpxs_tstc_vector cpxs_leq cpxs_lift cpxs_lleq cpxs_aaa cpxs_cpxs + fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )fpbs_lift fpbs_fleq fpbs_aaa fpbs_fpbs fpbs_ext
+
+
+ 		decomposed extended computationscpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?,?] ? )scpds_lift scpds_aaa scpds_scpds +
+
+
context-sensitive computationlprs ( ⦃?,?⦄ ⊢ ➡* ? )lprs_ldrop lprs_cprs lprs_lprs + context-sensitive extended computationlpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )lpxs_drop lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs
+
+
+
cprs ( ⦃?,?⦄ ⊢ ? ➡* ?)cprs_lift cprs_cprs + cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )cpxs_tsts cpxs_tsts_vector cpxs_leq cpxs_lift cpxs_lleq cpxs_aaa cpxs_cpxs
+
+
local env. ref. for abstract candidates of reducibilitylsubc ( ? ⊢ ? ⫃[?] ? )lsubc_ldrop lsubc_ldrops lsubc_lsuba + context-sensitive computationlprs ( ⦃?,?⦄ ⊢ ➡* ? )lprs_drop lprs_cprs lprs_lprs
+
+
support for abstract computation propertiesacpacp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )acp_aaa +
reduction"big tree" parallel reductionfpb ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )fpb_lift fpb_aaa + cprs ( ⦃?,?⦄ ⊢ ? ➡* ?)cprs_lift cprs_cprs
+
+
normal forms for context-sensitive extended reductioncnx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐍⦃?⦄ )cnx_lift cnx_crx cnx_cix + local env. ref. for generic reducibilitylsubc ( ? ⊢ ? ⫃[?] ? )lsubc_drop lsubc_drops lsubc_lsuba
+
+
context-sensitive extended reductionlpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )lpx_ldrop lpx_freeslpx_lleq lpx_aaa + support for generic computation propertiesgcpgcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )gcp_aaa
+ reduction"big tree" parallel reductionfpb ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )fpb_lift fpb_aaa +
+
+

cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )cpx_leq cpx_lift cpx_llpx_sn cpx_lleq cpx_cix + normal forms for context-sensitive extended reductioncnx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐍⦃?⦄ )cnx_lift cnx_crx cnx_cix
+
+
irreducible forms for context-sensitive extended reductioncix ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐈⦃?⦄ )cix_lift + context-sensitive extended reductionlpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )lpx_drop lpx_frees lpx_lleq lpx_aaa
+
+
reducible forms for context-sensitive extended reductioncrx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐑⦃?⦄ )crx_lift +
+ cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )cpx_leq cpx_lift cpx_llpx_sn cpx_lleq cpx_cix +
+
+
normal forms for context-sensitive reductioncnr ( ⦃?,?⦄ ⊢ ➡ 𝐍⦃?⦄ )cnr_lift cnr_crr cnr_cir + irreducible forms for context-sensitive extended reductioncix ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐈⦃?⦄ )cix_lift
+
+
context-sensitive reductionlpr ( ⦃?,?⦄ ⊢ ➡ ? )lpr_ldrop lpr_lpr + reducible forms for context-sensitive extended reductioncrx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐑⦃?⦄ )crx_lift
+
-
- 		+
cpr ( ⦃?,?⦄ ⊢ ? ➡ ? )cpr_lift cpr_llpx_sn cpr_cir + normal forms for context-sensitive reductioncnr ( ⦃?,?⦄ ⊢ ➡ 𝐍⦃?⦄ )cnr_lift cnr_crr cnr_cir
+
+
irreducible forms for context-sensitive reductioncir ( ⦃?,?⦄ ⊢ ➡ 𝐈⦃?⦄ )cir_lift + context-sensitive reductionlpr ( ⦃?,?⦄ ⊢ ➡ ? )lpr_drop lpr_lpr
+
+ +
+
reducible forms for context-sensitive reductioncrr ( ⦃?,?⦄ ⊢ ➡ 𝐑⦃?⦄ )crr_lift + cpr ( ⦃?,?⦄ ⊢ ? ➡ ? )cpr_lift cpr_llpx_sn cpr_cir
+
unfoldunfoldunfold ( ⦃?,?⦄ ⊢ ? ⧫* ? ) +
+ irreducible forms for context-sensitive reductioncir ( ⦃?,?⦄ ⊢ ➡ 𝐈⦃?⦄ )cir_lift
+
+
iterated static type assignmentlstas ( ⦃?,?⦄ ⊢ ? •*[?,?] ? )lstas_alt ( ⦃?,?⦄ ⊢ ? ••*[?,?] ? )lstas_lift lstas_aaa lstas_da lstas_lstas + reducible forms for context-sensitive reductioncrr ( ⦃?,?⦄ ⊢ ➡ 𝐑⦃?⦄ )crr_lift +
+
static typinglocal env. ref. for degree assignmentlsubd ( ? ⊢ ? ▪⫃ ? )lsubd_da lsubd_lsubd + unfoldunfoldunfold ( ⦃?,?⦄ ⊢ ? ⧫* ? ) +
+
+
+
degree assignmentda ( ⦃?,?⦄ ⊢ ? ▪[?,?] ? )da_lift da_aaa da_sta da_da + iterated static type assignmentlstas ( ⦃?,?⦄ ⊢ ? •*[?,?] ? )lstas_lift lstas_llpx_sn.ma lstas_aaa lstas_da lstas_lstas
+
-
- 		stratified equivalencesteq ( ? ≡[?,?] ? )steq_steq + static typinglocal env. ref. for degree assignmentlsubd ( ? ⊢ ? ⫃▪[?,?] ? )lsubd_da lsubd_lsubd
+
+
static type assignmentsta ( ⦃?,?⦄ ⊢ ? •[?] ? )sta_lift sta_lpx_sn sta_aaa sta_sta + degree assignmentda ( ⦃?,?⦄ ⊢ ? ▪[?,?] ? )da_lift da_aaa da_da
+
+
parametersshsd + parametersshsd
+
+
local env. ref. for atomic arity assignmentlsuba ( ? ⊢ ? ⁝⫃ ? )lsuba_aaa lsuba_lsuba + local env. ref. for atomic arity assignmentlsuba ( ? ⊢ ? ⫃⁝ ? )lsuba_aaa lsuba_lsuba
+
+
atomic arity assignmentaaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )aaa_lift aaa_lifts aaa_fqus aaa_lleq aaa_aaa + atomic arity assignmentaaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )aaa_lift aaa_lifts aaa_fqus aaa_lleq aaa_aaa
+
+
restricted local env. ref.lsubr ( ? ⫃ ? )lsubr_lsubr + restricted local env. ref.lsubr ( ? ⫃ ? )lsubr_lsubr
+
multiple substitutionlazy equivalencefleq ( ⦃?,?,?⦄ ≡[?] ⦃?,?,?⦄ )fleq_fleq + multiple substitutionlazy equivalencefleq ( ⦃?,?,?⦄ ≡[?] ⦃?,?,?⦄ )fleq_fleq
+
+
+
lleq ( ? ≡[?,?] ? )lleq_alt lleq_alt_rec lleq_leq lleq_ldrop lleq_fqus lleq_llor lleq_lleq + 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_ldrop llpx_sn_lpx_sn llpx_sn_frees llpx_sn_llor + 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_ldrop + pointwise union for local environmentsllor ( ? ⩖[?,?] ? ≡ ? )llor_alt llor_drop
+
+
context-sensitive exclusion from free variablesfrees ( ? ⊢ ? ϵ 𝐅*[?]⦃?⦄ )frees_append frees_leq frees_lift + context-sensitive exclusion from free variablesfrees ( ? ⊢ ? ϵ 𝐅*[?]⦃?⦄ )frees_append frees_leq frees_lift
+
+
contxt-sensitive extended multiple substitutioncpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? )cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? )cpys_lift cpys_cpys + contxt-sensitive extended multiple substitutioncpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? )cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? )cpys_lift cpys_cpys
+
iterated structural successor for closuresfqus ( ⦃?,?,?⦄ ⊐* ⦃?,?,?⦄ )fqus_alt fqus_fqus + iterated structural successor for closuresfqus ( ⦃?,?,?⦄ ⊐* ⦃?,?,?⦄ )fqus_alt fqus_fqus
+
+
+
fqup ( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ )fqup_fqup + fqup ( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ )fqup_fqup
+
+
iterated local env. slicingldrops ( ⇩*[?,?] ? ≡ ? )ldrops_ldrop ldrops_ldrops + iterated local env. slicingdrops ( ⇩*[?,?] ? ≡ ? )drops_drop drops_drops
+
+
generic term relocationlifts_vector ( ⇧*[?] ? ≡ ? )lifts_lift_vector + generic term relocationlifts_vector ( ⇧*[?] ? ≡ ? )lifts_lift_vector
+
+
+
lifts ( ⇧*[?] ? ≡ ? )lifts_lift lifts_lifts + lifts ( ⇧*[?] ? ≡ ? )lifts_lift lifts_lifts
+
+
support for generic relocationgr2 ( @⦃?,?⦄ ≡ ? )gr2_plus ( ? + ? )gr2_minus ( ? ▭ ? ≡ ? )gr2_gr2support for multiple relocationmr2 ( @⦃?,?⦄ ≡ ? )mr2_plus ( ? + ? )mr2_minus ( ? ▭ ? ≡ ? )mr2_mr2
substitutionstructural successor for closuresfquq ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ )fquq_alt ( ⦃?,?,?⦄ ⊐⊐⸮ ⦃?,?,?⦄ ) + substitutionstructural successor for closuresfquq ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ )fquq_alt ( ⦃?,?,?⦄ ⊐⊐⸮ ⦃?,?,?⦄ )
+
+
+
fqu ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ ) + fqu ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ )
+
+
+
global env. slicinggget ( ⇩[?] ? ≡ ? )gget_gget + global env. slicinggget ( ⇩[?] ? ≡ ? )gget_gget
+
+
contxt-sensitive extended ordinary substitutioncpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? )cpy_lift cpy_nlift cpy_cpy + contxt-sensitive extended ordinary substitutioncpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? )cpy_lift cpy_nlift cpy_cpy
+
+
local env. ref. for extended substitutionlsuby ( ? ⊑×[?,?] ? )lsuby_lsuby + local env. ref. for extended substitutionlsuby ( ? ⊆[?,?] ? )lsuby_lsuby
+
+
pointwise extension of a relationlpx_snlpx_sn_alt lpx_sn_tc lpx_sn_ldrop lpx_sn_lpx_sn + pointwise extension of a relationlpx_snlpx_sn_alt lpx_sn_tc lpx_sn_drop lpx_sn_lpx_sn
+
+
basic local env. slicingldrop ( ⇩[?,?,?] ? ≡ ? )ldrop_append ldrop_leq ldrop_ldrop + basic local env. slicingdrop ( ⇩[?,?,?] ? ≡ ? )drop_append drop_leq drop_drop
+
+
basic term relocationlift_vector ( ⇧[?,?] ? ≡ ? )lift_lift_vector + basic term relocationlift_vector ( ⇧[?,?] ? ≡ ? )lift_lift_vector
+
+
+
lift ( ⇧[?,?] ? ≡ ? )lift_neq lift_lift + lift ( ⇧[?,?] ? ≡ ? )lift_neq lift_lift
+
grammarequivalence for local environmentsleq ( ? ≃[?,?] ? )leq_leq + grammarequivalence for local environmentsleq ( ? ⩬[?,?] ? )leq_leq
+
+
same top term constructortstc ( ? ≃ ? )tstc_tstc tstc_vector + same top term structuretsts ( ? ≂ ? )tsts_tsts tsts_vector
+
+
closurescl_weight ( ♯{?,?,?} )cl_restricted_weight ( ♯{?,?} ) + closurescl_weight ( ♯{?,?,?} )cl_restricted_weight ( ♯{?,?} )
+
+
internal syntaxgenv + internal syntaxgenv
+
+
+
+
lenvlenv_weight ( ♯{?} )lenv_length ( |?| )lenv_append ( ? @@ ? )lenvlenv_weight ( ♯{?} )lenv_length ( |?| )lenv_append ( ? @@ ? )
+
+
termterm_weight ( ♯{?} )term_simple ( 𝐒⦃?⦄ )term_vectortermterm_weight ( ♯{?} )term_simple ( 𝐒⦃?⦄ )term_vector ( Ⓐ?.? )
+
+
item + item
+
+
+
external syntaxaarity + external syntaxaarity
+
+
-
Physical Structure of the Specification
+
Physical Structure of the Specification
The source files are grouped in directories, one for each component.
@@ -1286,6 +1319,6 @@

-
Last update: Sun, 15 Jun 2014 16:14:12 +0200
+
Last update: Wed, 10 Sep 2014 21:47:00 +0200