domain | block | leader | applicator (with →θ)* | reduction | →ζ * | reference * |
{X | Γ ⊢ X : W} | local typed abstraction * | Γ ⊢ +λW | ⓐV | →β | no | #i |
|
local typed declaration ** | Γ ⊢ -λW | ⓐV | →β | no | #i |
|
global typed declaration *** | Γ ⊢ pλW | no | no | no | $p |
|
native type annotation * | Γ ⊢ ⓝW | no | no | yes | no |
{X | Γ ⊢ X = V} | local abbreviation * | Γ ⊢ +δV | no | local →δ | yes | #i |
|
local definition ** | Γ ⊢ -δV | no | local →δ | no | #i |
|
global definition *** | Γ ⊢ pδV | no | global →δ | no | $p |
no | sort **** | Γ ⊢ ⋆k | no | no | no | no |
category | objects |
|
|
|
|
|
sizes | files | 324 | characters | 549104 | nodes | 1564238 |
propositions | theorems | 103 | lemmas | 1089 | total | 1192 |
concepts | declared | 50 | defined | 77 | total | 127 |
component | plane | files |
|
|
|
dynamic typing | local env. ref. for stratified native validity | lsubsv ( ? ⊢ ? ¡⊑[?,?] ? ) | lsubsv_ldrop lsubsv_lsubd lsubsv_lsuba lsubsv_lsstas lsubsv_cpds lsubsv_cpcs lsubsv_snv |
|
|
|
stratified native validity | snv ( ⦃?,?⦄ ⊢ ? ¡[?,?] ) | snv_lift snv_da_lpr snv_aaa snv_lsstas snv_lsstas_lpr snv_lpr snv_cpcs |
|
|
equivalence | decomposed extended equivalence | cpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?] ? ) | cpes_cpds |
|
|
|
context-sensitive equivalence | cpcs ( ⦃?,?⦄ ⊢ ? ⬌* ? ) | cpcs_aaa cpcs_cprs cpcs_cpcs |
|
|
conversion | context-sensitive conversion | cpc ( ⦃?,?⦄ ⊢ ? ⬌ ? ) | cpc_cpc |
|
|
computation | context-sensitive extended evaluation | cpxe ( ⦃?,?⦄ ⊢ ➡*[?,?] 𝐍⦃?⦄ ) |
|
|
|
|
context-sensitive evaluation | cpre ( ⦃?,?⦄ ⊢ ➡* 𝐍⦃?⦄ ) | cpre_cpre |
|
|
|
strongly normalizing "big tree" computation | fsb ( ⦃?,?⦄ ⊢ ⦥[?,?] ? ) | fsb_alt ( ⦃?,?⦄ ⊢ ⦥⦥[?,?] ? ) | fsb_aaa fsb_csx |
|
|
strongly normalizing extended computation | lsx ( ? ⊢ ⬊*[?,?,?] ? ) | lsx_cpxs lsx_csx |
|
|
|
|
csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? ) | csx_tstc_vector csx_aaa |
|
|
|
|
csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? ) | csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? ) | csx_lift csx_lpx csx_fpbs |
|
|
"big tree" parallel computation | fpbg ( ⦃?,?,?⦄ >⋕[?,?] ⦃?,?,?⦄ ) | fpbg_lift fpbg_fpns fpbg_fpbg |
|
|
|
|
fpbc ( ⦃?,?,?⦄ ≻⋕[?,?] ⦃?,?,?⦄ ) | fpbc_fpns fpbc_fpbs |
|
|
|
|
fpbu ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ ) | fpbu_lift fpbu_fpns |
|
|
|
|
fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ ) | fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ ) | fpbs_lift fpbs_aaa fpbs_fpns fpbs_fpbs |
|
|
parallel computation for "big tree" normal forms | fpns ( ⦃?,?,?⦄ ⊢ ⋕➡*[?,?] ⦃?,?,?⦄ ) | fpns_fpns |
|
|
|
decomposed extended computation | cpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?] ? ) | cpds_lift cpds_aaa cpds_cpds |
|
|
|
context-sensitive extended computation | lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? ) | lpxs_alt ( ⦃?,?⦄ ⊢ ➡➡*[?,?] ? ) | lpxs_ldrop lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs |
|
|
|
cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? ) | cpxs_tstc cpxs_tstc_vector cpxs_lift cpxs_cpys cpxs_lleq cpxs_aaa cpxs_cpxs |
|
|
|
context-sensitive computation | lprs ( ⦃?,?⦄ ⊢ ➡* ? ) | lprs_alt ( ⦃?,?⦄ ⊢ ➡➡* ? ) | lprs_ldrop lprs_cprs lprs_lprs |
|
|
|
cprs ( ⦃?,?⦄ ⊢ ? ➡* ?) | cprs_lift cprs_cprs |
|
|
|
local env. ref. for abstract candidates of reducibility | lsubc ( ? ⊢ ? ⊑[?] ? ) | lsubc_ldrop lsubc_ldrops lsubc_lsuba |
|
|
|
support for abstract computation properties | acp | acp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 ) | acp_aaa |
|
reduction | "big tree" parallel reduction | fpb ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ ) | fpb_lift fpb_aaa |
|
|
|
context-sensitive extended normal forms | cnx ( ⦃?,?⦄ ⊢ 𝐍[?,?]⦃?⦄ ) | cnx_lift cnx_crx cnx_cix |
|
|
|
context-sensitive extended reduction | lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? ) | lpx_ldrop lpx_lleq lpx_aaa |
|
|
|
|
cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? ) | cpx_lift cpx_cpys cpx_lleq cpx_cix |
|
|
|
context-sensitive extended irreducible forms | cix ( ⦃?,?⦄ ⊢ 𝐈[?,?]⦃?⦄ ) | cix_append cix_lift |
|
|
|
context-sensitive extended reducible forms | crx ( ⦃?,?⦄ ⊢ 𝐑[?,?]⦃?⦄ ) | crx_append crx_lift |
|
|
|
context-sensitive normal forms | cnr ( ⦃?,?⦄ ⊢ 𝐍⦃?⦄ ) | cnr_lift cnr_crr cnr_cir |
|
|
|
context-sensitive reduction | lpr ( ⦃?,?⦄ ⊢ ➡ ? ) | lpr_ldrop lpr_lpr |
|
|
|
|
cpr ( ⦃?,?⦄ ⊢ ? ➡ ? ) | cpr_lift cpr_cir |
|
|
|
context-sensitive irreducible forms | cir ( ⦃?,?⦄ ⊢ 𝐈⦃?⦄ ) | cir_append cir_lift |
|
|
|
context-sensitive reducible forms | crr ( ⦃?,?⦄ ⊢ 𝐑⦃?⦄ ) | crr_append crr_lift |
|
|
unfold | unfold | unfold ( ⦃?,?⦄ ⊢ ? ⧫* ? ) |
|
|
|
|
iterated static type assignment | lsstas ( ⦃?,?⦄ ⊢ ? •*[?,?,?] ? ) | lsstas_alt ( ⦃?,?⦄ ⊢ ? ••*[?,?,?] ? ) | lsstas_lift lsstas_aaa lsstas_lsstas |
|
static typing | local env. ref. for atomic arity assignment | lsuba ( ? ⊢ ? ⁝⊑ ? ) | lsuba_ldrop lsuba_aaa lsuba_lsuba |
|
|
|
atomic arity assignment | aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? ) | aaa_lift aaa_lifts aaa_fqus aaa_da aaa_ssta aaa_aaa |
|
|
|
stratified static type assignment | ssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? ) | ssta_lift ssta_ssta |
|
|
|
local env. ref. for degree assignment | lsubd ( ? ⊢ ? ▪⊑ ? ) | lsubd_da lsubd_lsubd |
|
|
|
degree assignment | da ( ⦃?,?⦄ ⊢ ? ▪[?,?] ? ) | da_lift da_da |
|
|
|
parameters | sh | sd |
|
|
substitution | lazy equivalence for local environments | lleq ( ? ⋕[?,?] ? ) | lleq_alt ( ? ⋕⋕[?,?] ? ) | lleq_ldrop lleq_fqus lleq_lleq lleq_ext |
|
|
contxt-sensitive extended multiple substitution | cpys ( ⦃?,?⦄ ⊢ ? ▶*×[?,?] ? ) | cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*×[?,?] ? ) | cpys_lift cpys_cpys |
|
|
iterated structural successor for closures | fqus ( ⦃?,?,?⦄ ⊃* ⦃?,?,?⦄ ) | fqus_alt fqus_fqus |
|
|
|
|
fqup ( ⦃?,?,?⦄ ⊃+ ⦃?,?,?⦄ ) | fqup_fqup |
|
|
|
iterated local env. slicing | ldrops ( ⇩*[?,?] ? ≡ ? ) | ldrops_ldrop ldrops_ldrops |
|
|
|
generic term relocation | lifts_vector ( ⇧*[?] ? ≡ ? ) | lifts_lift_vector |
|
|
|
|
lifts ( ⇧*[?] ? ≡ ? ) | lifts_lift lifts_lifts |
|
|
|
support for generic relocation | gr2 ( @⦃?,?⦄ ≡ ? ) | gr2_plus ( ? + ? ) | gr2_minus ( ? ▭ ? ≡ ? ) | gr2_gr2 |
relocation | contxt-sensitive extended ordinary substitution | cpy ( ⦃?,?⦄ ⊢ ? ▶×[?,?] ? ) | cpy_lift cpy_cpy |
|
|
|
local env. ref. for extended substitution | lsuby ( ? ⊑×[?,?] ? ) | lsuby_lsuby |
|
|
|
restricted local env. ref. | lsubr ( ? ⊑ ? ) | lsubr_lsubr |
|
|
|
structural successor for closures | fquq ( ⦃?,?,?⦄ ⊃⸮ ⦃?,?,?⦄ ) | fquq_alt ( ⦃?,?,?⦄ ⊃⊃⸮ ⦃?,?,?⦄ ) |
|
|
|
|
fqu ( ⦃?,?,?⦄ ⊃ ⦃?,?,?⦄ ) |
|
|
|
|
global env. slicing | gdrop ( ⇩[?] ? ≡ ? ) | gdrop_gdrop |
|
|
|
basic local env. slicing | ldrop ( ⇩[?,?,?] ? ≡ ? ) | ldrop_append ldrop_lpx_sn ldrop_ldrop |
|
|
|
basic term relocation | lift_vector ( ⇧[?,?] ? ≡ ? ) | lift_lift_vector |
|
|
|
|
lift ( ⇧[?,?] ? ≡ ? ) | lift_lift |
|
|
grammar | pointwise extension of a relation | lpx_sn | lpx_sn_tc lpx_sn_lpx_sn |
|
|
|
same top term constructor | tstc ( ? ≃ ? ) | tstc_tstc tstc_vector |
|
|
|
closures | cl_shift ( ? @@ ? ) | cl_weight ( ♯{?,?,?} ) |
|
|
|
internal syntax | genv |
|
|
|
|
|
lenv | lenv_weight ( ♯{?} ) | lenv_length ( |?| ) | lenv_append ( ? @@ ? ) |
|
|
term | term_weight ( ♯{?} ) | term_simple ( 𝐒⦃?⦄ ) | term_vector |
|
|
item |
|
|
|
|
external syntax | aarity |
|
|
|