- | component |
- plane |
- files |
-
+ | component |
+ plane |
+ files |
+
|
-
+ |
|
-
+ |
|
- | examples |
- |
- ex_cpr_omega |
-
+ | examples |
+ terms with special features |
+ ex_sta_ldec ex_cpr_omega ex_fpbg_refl |
+
|
-
+ |
|
-
+ |
|
- |
- |
- |
-
+ | |
+ |
+ |
+
|
-
+ |
|
-
+ |
|
- | dynamic typing |
- local env. ref. for stratified native validity |
- lsubsv ( ? ⢠? ¡â«[?,?] ? ) |
- lsubsv_lsuba lsubsv_lsubd lsubsv_lstas lsubsv_cpds lsubsv_cpcs lsubsv_snv |
-
+ | dynamic typing |
+ local env. ref. for stratified native validity |
+ lsubsv ( ? ⢠? â«Â¡[?,?] ? ) |
+ lsubsv_lsuba lsubsv_lsubd lsubsv_lstas lsubsv_scpds lsubsv_cpcs lsubsv_snv |
+
|
-
+ |
|
-
-
- |
- stratified native validity |
- snv ( �,?⦠⢠? ¡[?,?] ) |
- snv_lift snv_aaa snv_da_lpr snv_lstas snv_lstas_lpr snv_lpr snv_cpcs snv_preserve |
-
+ |
|
-
+ | stratified native validity |
+ shnv ( �,?⦠⢠? ¡[?,?,?] ) |
+
|
-
-
- | equivalence |
- decomposed extended equivalence |
- cpes ( â¦?,?⦠⢠? â¢*â¬*[?,?] ? ) |
- cpes_cpds |
-
+ |
|
-
+ |
|
- |
+ |
|
- context-sensitive equivalence |
- cpcs ( â¦?,?⦠⢠? â¬* ? ) |
- cpcs_aaa cpcs_cprs cpcs_cpcs |
-
+ |
|
-
+ | snv ( �,?⦠⢠? ¡[?,?] ) |
+ snv_lift snv_aaa snv_da_lpr snv_lstas snv_lstas_lpr snv_lpr snv_scpes snv_preserve |
+
|
-
-
- | conversion |
- context-sensitive conversion |
- cpc ( �,?⦠⢠? ⬠? ) |
- cpc_cpc |
-
-
- |
-
+ |
|
- | computation |
- evaluation for context-sensitive extended reduction |
- cpxe ( â¦?,?⦠⢠â¡*[?,?] ðâ¦?⦠) |
-
-
- |
-
+ | equivalence |
+ decomposed extended equivalence |
+ scpes ( â¦?,?⦠⢠? â¢*â¬*[?,?,?,?] ? ) |
+ scpes_aaa scpes_cpcs scpes_scpes |
+
|
-
+ |
|
- |
+ |
|
- evaluation for context-sensitive reduction |
- cpre ( â¦?,?⦠⢠â¡* ðâ¦?⦠) |
- cpre_cpre |
-
+ | context-sensitive equivalence |
+ cpcs ( â¦?,?⦠⢠? â¬* ? ) |
+ cpcs_aaa cpcs_cprs cpcs_cpcs |
+
|
-
+ |
|
- |
+ | conversion |
+ context-sensitive conversion |
+ cpc ( �,?⦠⢠? ⬠? ) |
+ cpc_cpc |
+
|
- strongly normalizing "big tree" computation |
- fsb ( �,?⦠⢠⦥[?,?] ? ) |
- fsb_alt ( �,?⦠⢠⦥⦥[?,?] ? ) |
- fsb_aaa fsb_csx |
-
+ |
|
- |
+ | computation |
+ evaluation for context-sensitive extended reduction |
+ cpxe ( â¦?,?⦠⢠â¡*[?,?] ðâ¦?⦠) |
+
|
- strongly normalizing extended computation |
- lcosx ( ? ⢠~â¬*[?,?,?] ? ) |
- lcosx_cpx |
-
+ |
|
-
+ |
|
- |
+ |
|
-
+ | evaluation for context-sensitive reduction |
+ cpre ( â¦?,?⦠⢠â¡* ðâ¦?⦠) |
+ cpre_cpre |
+
|
- lsx ( ? ⢠â¬*[?,?,?,?] ? ) |
- lsx_alt ( ? ⢠â¬â¬*[?,?,?,?] ? ) |
- lsx_drop lsx_lpx lsx_lpxs llsx_csx |
-
+ |
|
- |
+ |
+
+ |
+ strongly normalizing qrst-computation |
+ fsb ( �,?⦠⢠⦥[?,?] ? ) |
+ fsb_alt ( �,?⦠⢠⦥⦥[?,?] ? ) |
+ fsb_aaa fsb_csx |
+
|
-
+ |
+
+
|
- csx_vector ( â¦?,?⦠⢠â¬*[?,?] ? ) |
- csx_tstc_vector csx_aaa |
-
+ | strongly normalizing extended computation |
+ lcosx ( ? ⢠~â¬*[?,?,?] ? ) |
+ lcosx_cpx |
+
|
-
+ |
|
- |
+ |
|
-
+ |
|
- csx ( â¦?,?⦠⢠â¬*[?,?] ? ) |
- csx_alt ( â¦?,?⦠⢠â¬â¬*[?,?] ? ) |
- csx_lift csx_lleq csx_lpx csx_lpxs csx_fpbs |
-
+ | lsx ( ? ⢠â¬*[?,?,?,?] ? ) |
+ lsx_alt ( ? ⢠â¬â¬*[?,?,?,?] ? ) |
+ lsx_drop lsx_lpx lsx_lpxs llsx_csx |
+
|
- |
+ |
|
- "big tree" parallel computation |
- fpbg ( â¦?,?,?⦠>â¡[?,?] â¦?,?,?⦠) |
- fpbg_lift fpbg_fleq fpbg_fpbg |
-
+ |
|
-
+ | csx_vector ( â¦?,?⦠⢠â¬*[?,?] ? ) |
+ csx_tsts_vector csx_aaa |
+
|
-
-
- |
+ |
|
-
+ |
+
+
|
- fpbc ( â¦?,?,?⦠â»â¡[?,?] â¦?,?,?⦠) |
- fpbc_fleq fpbc_fpbs |
-
+ |
|
-
+ | csx ( â¦?,?⦠⢠â¬*[?,?] ? ) |
+ csx_alt ( â¦?,?⦠⢠â¬â¬*[?,?] ? ) |
+ csx_lift csx_lleq csx_lpx csx_lpxs csx_fpbs |
+
|
- |
+ |
|
-
+ | parallel qrst-computation |
+ fpbg ( â¦?,?,?⦠>â¡[?,?] â¦?,?,?⦠) |
+ fpbg_lift fpbg_fleq fpbg_fpbs fpbg_fpbg |
+
|
- fpbu ( â¦?,?,?⦠â»[?,?] â¦?,?,?⦠) |
- fpbu_lift fpbu_lleq |
- fpbu_fleq |
-
+ |
|
- |
+ |
|
-
+ |
|
- fpbs ( â¦?,?,?⦠â¥[?,?] â¦?,?,?⦠) |
- fpbs_alt ( â¦?,?,?⦠â¥â¥[?,?] â¦?,?,?⦠) |
- fpbs_lift fpbs_fleq fpbs_aaa fpbs_fpbs fpbs_ext |
-
+ | fpbs ( â¦?,?,?⦠â¥[?,?] â¦?,?,?⦠) |
+ fpbs_alt ( â¦?,?,?⦠â¥â¥[?,?] â¦?,?,?⦠) |
+ fpbs_lift fpbs_aaa fpbs_fpb fpbs_fpbs |
+
|
- |
+ |
|
- decomposed extended computation |
- cpds ( â¦?,?⦠⢠? â¢*â¡*[?,?] ? ) |
- cpds_lift cpds_aaa cpds_cpds |
-
+ | decomposed extended computation |
+ scpds ( â¦?,?⦠⢠? â¢*â¡*[?,?,?] ? ) |
+ scpds_lift scpds_aaa scpds_scpds |
+
|
-
+ |
|
- |
+ |
|
- context-sensitive extended computation |
- lpxs ( â¦?,?⦠⢠â¡*[?,?] ? ) |
- lpxs_drop lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs |
-
+ | context-sensitive extended computation |
+ lpxs ( â¦?,?⦠⢠â¡*[?,?] ? ) |
+ 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 |
-
+ | cpxs ( â¦?,?⦠⢠? â¡*[?,?] ? ) |
+ cpxs_tsts cpxs_tsts_vector cpxs_leq cpxs_lift cpxs_lleq cpxs_aaa cpxs_cpxs |
+
|
-
+ |
|
- |
+ |
|
- context-sensitive computation |
- lprs ( â¦?,?⦠⢠â¡* ? ) |
- lprs_drop lprs_cprs lprs_lprs |
-
+ | context-sensitive computation |
+ lprs ( â¦?,?⦠⢠â¡* ? ) |
+ lprs_drop lprs_cprs lprs_lprs |
+
|
-
+ |
|
- |
+ |
|
-
+ |
|
- cprs ( â¦?,?⦠⢠? â¡* ?) |
- cprs_lift cprs_cprs |
-
+ | cprs ( â¦?,?⦠⢠? â¡* ?) |
+ cprs_lift cprs_cprs |
+
|
-
+ |
|
- |
+ |
|
- local env. ref. for abstract candidates of reducibility |
- lsubc ( ? ⢠? â«[?] ? ) |
- lsubc_drop lsubc_drops lsubc_lsuba |
-
+ | local env. ref. for generic reducibility |
+ lsubc ( ? ⢠? â«[?] ? ) |
+ lsubc_drop lsubc_drops lsubc_lsuba |
+
|
-
+ |
|
- |
+ |
+
+ |
+ support for generic computation properties |
+ gcp |
+ gcp_cr ( â¦?,?,?⦠ϵ[?] ã?ã ) |
+ gcp_aaa |
+
|
- support for abstract computation properties |
- acp |
- acp_cr ( â¦?,?,?⦠ϵ[?] ã?ã ) |
- acp_aaa |
-
+ |
+
+ | reduction |
+ parallel qrst-reduction |
+ fpbq ( â¦?,?,?⦠â½[?,?] â¦?,?,?⦠) |
+ fpbq_alt ( â¦?,?,?⦠â½â½[?,?] â¦?,?,?⦠) |
+ fpbq_lift fpbq_aaa |
+
|
- | reduction |
- "big tree" parallel reduction |
- fpb ( â¦?,?,?⦠â½[?,?] â¦?,?,?⦠) |
- fpb_lift fpb_aaa |
-
+ |
+
+ |
+
|
-
+ | fpb ( â¦?,?,?⦠â»[?,?] â¦?,?,?⦠) |
+ fpb_lift fpb_lleq fpb_fleq |
+
+
+ |
+
|
- |
+ |
|
- normal forms for context-sensitive extended reduction |
- cnx ( â¦?,?⦠⢠â¡[?,?] ðâ¦?⦠) |
- cnx_lift cnx_crx cnx_cix |
-
+ | normal forms for context-sensitive extended reduction |
+ cnx ( â¦?,?⦠⢠â¡[?,?] ðâ¦?⦠) |
+ cnx_lift cnx_crx cnx_cix |
+
|
-
+ |
|
- |
+ |
|
- context-sensitive extended reduction |
- lpx ( â¦?,?⦠⢠â¡[?,?] ? ) |
- lpx_drop lpx_frees |
- lpx_lleq lpx_aaa |
-
+ | context-sensitive extended reduction |
+ lpx ( â¦?,?⦠⢠â¡[?,?] ? ) |
+ lpx_drop lpx_frees lpx_lleq lpx_aaa |
+
+
+ |
+
|
- |
+ |
|
-
+ |
|
- cpx ( â¦?,?⦠⢠? â¡[?,?] ? ) |
- cpx_leq cpx_lift cpx_llpx_sn cpx_lleq cpx_cix |
-
+ | cpx ( â¦?,?⦠⢠? â¡[?,?] ? ) |
+ cpx_leq cpx_lift cpx_llpx_sn cpx_lleq cpx_cix |
+
|
-
+ |
|
- |
+ |
|
- irreducible forms for context-sensitive extended reduction |
- cix ( â¦?,?⦠⢠â¡[?,?] ðâ¦?⦠) |
- cix_lift |
-
+ | irreducible forms for context-sensitive extended reduction |
+ cix ( â¦?,?⦠⢠â¡[?,?] ðâ¦?⦠) |
+ cix_lift |
+
|
-
+ |
|
- |
+ |
|
- reducible forms for context-sensitive extended reduction |
- crx ( â¦?,?⦠⢠â¡[?,?] ðâ¦?⦠) |
- crx_lift |
-
+ | reducible forms for context-sensitive extended reduction |
+ crx ( â¦?,?⦠⢠â¡[?,?] ðâ¦?⦠) |
+ crx_lift |
+
|
-
+ |
|
- |
+ |
|
- normal forms for context-sensitive reduction |
- cnr ( â¦?,?⦠⢠⡠ðâ¦?⦠) |
- cnr_lift cnr_crr cnr_cir |
-
+ | normal forms for context-sensitive reduction |
+ cnr ( â¦?,?⦠⢠⡠ðâ¦?⦠) |
+ cnr_lift cnr_crr cnr_cir |
+
|
-
+ |
|
- |
+ |
|
- context-sensitive reduction |
- lpr ( �,?⦠⢠⡠? ) |
- lpr_drop lpr_lpr |
-
+ | context-sensitive reduction |
+ lpr ( �,?⦠⢠⡠? ) |
+ lpr_drop lpr_lpr |
+
|
-
+ |
|
- |
+ |
|
-
+ |
|
- cpr ( �,?⦠⢠? ⡠? ) |
- cpr_lift cpr_llpx_sn cpr_cir |
-
+ | cpr ( �,?⦠⢠? ⡠? ) |
+ cpr_lift cpr_llpx_sn cpr_cir |
+
|
-
+ |
|
- |
+ |
|
- irreducible forms for context-sensitive reduction |
- cir ( â¦?,?⦠⢠⡠ðâ¦?⦠) |
- cir_lift |
-
+ | irreducible forms for context-sensitive reduction |
+ cir ( â¦?,?⦠⢠⡠ðâ¦?⦠) |
+ cir_lift |
+
|
-
+ |
|
- |
+ |
|
- reducible forms for context-sensitive reduction |
- crr ( â¦?,?⦠⢠⡠ðâ¦?⦠) |
- crr_lift |
-
+ | reducible forms for context-sensitive reduction |
+ crr ( â¦?,?⦠⢠⡠ðâ¦?⦠) |
+ crr_lift |
+
|
-
+ |
|
- | unfold |
- unfold |
- unfold ( �,?⦠⢠? ⧫* ? ) |
-
+ | unfold |
+ unfold |
+ unfold ( �,?⦠⢠? ⧫* ? ) |
+
|
-
+ |
|
-
+ |
|
-
-
- |
- iterated static type assignment |
- lstas ( â¦?,?⦠⢠? â¢*[?,?] ? ) |
- lstas_alt ( â¦?,?⦠⢠? â¢â¢*[?,?] ? ) |
- lstas_lift lstas_aaa lstas_da lstas_lstas |
-
+ |
|
-
-
- | static typing |
- local env. ref. for degree assignment |
- lsubd ( ? ⢠? âªâ« ? ) |
- lsubd_da lsubd_lsubd |
-
+ | iterated static type assignment |
+ lstas ( â¦?,?⦠⢠? â¢*[?,?] ? ) |
+ lstas_lift lstas_llpx_sn.ma lstas_aaa lstas_da lstas_lstas |
+
|
-
+ |
|
-
-
- |
- degree assignment |
- da ( â¦?,?⦠⢠? âª[?,?] ? ) |
- da_lift da_aaa da_sta da_da |
-
+ | static typing |
+ local env. ref. for degree assignment |
+ lsubd ( ? ⢠? â«âª[?,?] ? ) |
+ lsubd_da lsubd_lsubd |
+
|
-
+ |
|
- |
+ |
|
- static type assignment |
- sta ( â¦?,?⦠⢠? â¢[?] ? ) |
- sta_lift sta_lpx_sn sta_aaa sta_sta |
-
+ | degree assignment |
+ da ( â¦?,?⦠⢠? âª[?,?] ? ) |
+ da_lift da_aaa da_da |
+
|
-
+ |
|
- |
+ |
|
- parameters |
- sh |
- sd |
-
+ | parameters |
+ sh |
+ sd |
+
|
-
+ |
|
- |
+ |
|
- local env. ref. for atomic arity assignment |
- lsuba ( ? ⢠? ââ« ? ) |
- lsuba_aaa lsuba_lsuba |
-
+ | local env. ref. for atomic arity assignment |
+ lsuba ( ? ⢠? â«â ? ) |
+ lsuba_aaa lsuba_lsuba |
+
|
-
+ |
|
- |
+ |
|
- atomic arity assignment |
- aaa ( â¦?,?⦠⢠? â ? ) |
- aaa_lift aaa_lifts aaa_fqus aaa_lleq aaa_aaa |
-
+ | atomic arity assignment |
+ aaa ( â¦?,?⦠⢠? â ? ) |
+ 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 substitution |
- lazy equivalence |
- fleq ( â¦?,?,?⦠â¡[?] â¦?,?,?⦠) |
- fleq_fleq |
-
+ | multiple substitution |
+ lazy equivalence |
+ fleq ( â¦?,?,?⦠â¡[?] â¦?,?,?⦠) |
+ fleq_fleq |
+
|
-
+ |
|
- |
+ |
|
-
+ |
|
- lleq ( ? â¡[?,?] ? ) |
- lleq_alt lleq_alt_rec lleq_leq lleq_drop 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 relation |
- llpx_sn |
- llpx_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 |
-
+ | lazy pointwise extension of a relation |
+ llpx_sn |
+ llpx_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 environments |
- llor ( ? â©[?,?] ? â¡ ? ) |
- llor_alt llor_drop |
-
+ | pointwise union for local environments |
+ llor ( ? â[?,?] ? â¡ ? ) |
+ llor_alt llor_drop |
+
|
-
+ |
|
- |
+ |
|
- context-sensitive exclusion from free variables |
- frees ( ? ⢠? ϵ ð
*[?]�⦠) |
- frees_append frees_leq frees_lift |
-
+ | context-sensitive exclusion from free variables |
+ frees ( ? ⢠? ϵ ð
*[?]�⦠) |
+ frees_append frees_leq frees_lift |
+
|
-
+ |
|
- |
+ |
|
- contxt-sensitive extended multiple substitution |
- cpys ( â¦?,?⦠⢠? â¶*[?,?] ? ) |
- cpys_alt ( â¦?,?⦠⢠? â¶â¶*[?,?] ? ) |
- cpys_lift cpys_cpys |
-
+ | contxt-sensitive extended multiple substitution |
+ cpys ( â¦?,?⦠⢠? â¶*[?,?] ? ) |
+ cpys_alt ( â¦?,?⦠⢠? â¶â¶*[?,?] ? ) |
+ cpys_lift cpys_cpys |
+
|
- |
+ |
|
- iterated structural successor for closures |
- fqus ( â¦?,?,?⦠â* â¦?,?,?⦠) |
- fqus_alt fqus_fqus |
-
+ | iterated structural successor for closures |
+ fqus ( â¦?,?,?⦠â* â¦?,?,?⦠) |
+ fqus_alt fqus_fqus |
+
|
-
+ |
|
- |
+ |
|
-
+ |
|
- fqup ( â¦?,?,?⦠â+ â¦?,?,?⦠) |
- fqup_fqup |
-
+ | fqup ( â¦?,?,?⦠â+ â¦?,?,?⦠) |
+ fqup_fqup |
+
|
-
+ |
|
- |
+ |
|
- iterated local env. slicing |
- drops ( â©*[?,?] ? â¡ ? ) |
- drops_drop drops_drops |
-
+ | iterated local env. slicing |
+ drops ( â¬*[?,?] ? â¡ ? ) |
+ drops_drop drops_drops |
+
|
-
+ |
|
- |
+ |
|
- generic term relocation |
- lifts_vector ( â§*[?] ? â¡ ? ) |
- lifts_lift_vector |
-
+ | generic term relocation |
+ lifts_vector ( â¬*[?] ? â¡ ? ) |
+ lifts_lift_vector |
+
|
-
+ |
|
- |
+ |
|
-
+ |
|
- lifts ( â§*[?] ? â¡ ? ) |
- lifts_lift lifts_lifts |
-
+ | lifts ( â¬*[?] ? â¡ ? ) |
+ lifts_lift lifts_lifts |
+
|
-
+ |
|
- |
+ |
|
- support for generic relocation |
- gr2 ( @�,?⦠⡠? ) |
- gr2_plus ( ? + ? ) |
- gr2_minus ( ? â ? â¡ ? ) |
- gr2_gr2 |
+ support for multiple relocation |
+ mr2 ( @�,?⦠⡠? ) |
+ mr2_plus ( ? + ? ) |
+ mr2_minus ( ? â ? â¡ ? ) |
+ mr2_mr2 |
- | substitution |
- structural successor for closures |
- fquq ( â¦?,?,?⦠â⸮ â¦?,?,?⦠) |
- fquq_alt ( â¦?,?,?⦠ââ⸮ â¦?,?,?⦠) |
-
+ | substitution |
+ structural successor for closures |
+ fquq ( â¦?,?,?⦠â⸮ â¦?,?,?⦠) |
+ fquq_alt ( â¦?,?,?⦠ââ⸮ â¦?,?,?⦠) |
+
|
-
+ |
|
- |
+ |
|
-
+ |
|
- fqu ( â¦?,?,?⦠â â¦?,?,?⦠) |
-
+ | fqu ( â¦?,?,?⦠â â¦?,?,?⦠) |
+
|
-
+ |
|
-
+ |
|
- |
+ |
|
- global env. slicing |
- gget ( â©[?] ? â¡ ? ) |
- gget_gget |
-
+ | global env. slicing |
+ gget ( â¬[?] ? â¡ ? ) |
+ gget_gget |
+
|
-
+ |
|
- |
+ |
|
- contxt-sensitive extended ordinary substitution |
- cpy ( â¦?,?⦠⢠? â¶[?,?] ? ) |
- cpy_lift cpy_nlift cpy_cpy |
-
+ | contxt-sensitive extended ordinary substitution |
+ cpy ( â¦?,?⦠⢠? â¶[?,?] ? ) |
+ cpy_lift cpy_nlift cpy_cpy |
+
|
-
+ |
|
- |
+ |
|
- local env. ref. for extended substitution |
- lsuby ( ? âÃ[?,?] ? ) |
- lsuby_lsuby |
-
+ | local env. ref. for extended substitution |
+ lsuby ( ? â[?,?] ? ) |
+ lsuby_lsuby |
+
|
-
+ |
|
- |
+ |
|
- pointwise extension of a relation |
- lpx_sn |
- lpx_sn_alt lpx_sn_tc lpx_sn_drop lpx_sn_lpx_sn |
-
+ | pointwise extension of a relation |
+ lpx_sn |
+ lpx_sn_alt lpx_sn_tc lpx_sn_drop lpx_sn_lpx_sn |
+
|
-
+ |
|
- |
+ |
|
- basic local env. slicing |
- drop ( â©[?,?,?] ? â¡ ? ) |
- drop_append drop_leq drop_drop |
-
+ | basic local env. slicing |
+ drop ( â¬[?,?,?] ? â¡ ? ) |
+ drop_append drop_leq drop_drop |
+
|
-
+ |
|
- |
+ |
|
- basic term relocation |
- lift_vector ( â§[?,?] ? â¡ ? ) |
- lift_lift_vector |
-
+ | basic term relocation |
+ lift_vector ( â¬[?,?] ? â¡ ? ) |
+ lift_lift_vector |
+
|
-
+ |
|
- |
+ |
|
-
+ |
|
- lift ( â§[?,?] ? â¡ ? ) |
- lift_neq lift_lift |
-
+ | lift ( â¬[?,?] ? â¡ ? ) |
+ lift_neq lift_lift |
+
|
-
+ |
|
- | grammar |
- equivalence for local environments |
- leq ( ? ⩬[?,?] ? ) |
- leq_leq |
-
+ | grammar |
+ equivalence for local environments |
+ leq ( ? ⩬[?,?] ? ) |
+ leq_leq |
+
|
-
+ |
|
- |
+ |
|
- same top term constructor |
- tstc ( ? â ? ) |
- tstc_tstc tstc_vector |
-
+ | same top term structure |
+ tsts ( ? â ? ) |
+ tsts_tsts tsts_vector |
+
|
-
+ |
|
- |
+ |
|
- closures |
- cl_weight ( â¯{?,?,?} ) |
- cl_restricted_weight ( â¯{?,?} ) |
-
+ | closures |
+ cl_weight ( â¯{?,?,?} ) |
+ cl_restricted_weight ( â¯{?,?} ) |
+
|
-
+ |
|
- |
+ |
|
- internal syntax |
- genv |
-
+ | internal syntax |
+ genv |
+
|
-
+ |
|
-
+ |
|
- |
+ |
|
-
+ |
|
- lenv |
- lenv_weight ( â¯{?} ) |
- lenv_length ( |?| ) |
- lenv_append ( ? @@ ? ) |
+ lenv |
+ lenv_weight ( â¯{?} ) |
+ lenv_length ( |?| ) |
+ lenv_append ( ? @@ ? ) |
- |
+ |
|
-
+ |
|
- term |
- term_weight ( â¯{?} ) |
- term_simple ( ðâ¦?⦠) |
- term_vector |
+ term |
+ term_weight ( â¯{?} ) |
+ term_simple ( ðâ¦?⦠) |
+ term_vector ( �.? ) |
- |
+ |
|
-
+ |
|
- item |
-
+ | item |
+
|
-
+ |
|
-
+ |
|
- |
+ |
|
- external syntax |
- aarity |
-
+ | external syntax |
+ aarity |
+
|
-
+ |
|
-
+ |
|
@@ -1272,8 +1273,7 @@