category | objects |
|
|
|
|
|
sizes | files | 212 | characters | 213959 | nodes | 1057531 |
propositions | theorems | 62 | lemmas | 741 | total | 803 |
concepts | declared | 31 | defined | 78 | total | 109 |
component | plane | files |
|
rt-transition | counted context-sensitive rt-transition | cpg ( ⦃?,?⦄ ⊢ ? ⬈[?,?] ? ) | cpg_simple cpg_drops cpg_lsubr |
iterated static typing | iterated extension on referred entries | tc_lfxs ( ? ⦻**[?,?] ? ) | tc_lfxs_length tc_lfxs_drops tc_lfxs_fqup tc_lfxs_tc_lfxs |
static typing | generic reducibility | lsubc ( ? ⊢ ? ⫃[?] ? ) | lsubc_drops lsubc_lsubr lsubc_lsuba |
|
|
gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 ) | gcp_aaa |
|
|
gcp |
|
|
atomic arity assignment | lsuba ( ? ⊢ ? ⫃⁝ ? ) | lsuba_drops lsuba_lsubr lsuba_aaa lsuba_lsuba |
|
|
aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? ) | aaa_drops aaa_fqus aaa_lfdeq aaa_aaa |
|
degree-based equivalence on referred entries | ffdeq ( ⦃?,?,?⦄ ≡[?,?] ⦃?,?,?⦄ ) | ffdeq_fqup ffdeq_ffdeq |
|
|
lfdeq ( ? ≡[?,?,?] ? ) | lfdeq_length lfdeq_drops lfdeq_fqup lfdeq_fqus lfdeq_lfdeq |
|
generic extension on referred entries | lfxs ( ? ⦻*[?,?] ? ) | lfxs_length lfxs_drops lfxs_fqup lfxs_lfxs |
|
context-sensitive free variables | lsubf ( ⦃?,?⦄ ⫃𝐅* ⦃?,?⦄ ) | lsubf_lsubr lsubf_frees lsubf_lsubf |
|
|
frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? ) | frees_drops frees_fqup frees_frees |
|
restricted ref. for local env. | lsubr ( ? ⫃ ? ) | lsubr_length lsubr_drops lsubr_lsubr |
s-computation | iterated structural successor for closures | fqus ( ⦃?,?,?⦄ ⊐*[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐* ⦃?,?,?⦄ ) | fqus_weight fqus_drops fqus_fqup fqus_fqus |
|
|
fqup ( ⦃?,?,?⦄ ⊐+[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ ) | fqup_weight fqup_drops fqup_fqup |
s-transition | structural successor for closures | fquq ( ⦃?,?,?⦄ ⊐⸮[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ ) | fquq_length fquq_weight |
|
|
fqu ( ⦃?,?,?⦄ ⊐[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ ) | fqu_length fqu_weight |
relocation | generic slicing for local environments | drops_vector ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? ) |
|
|
|
drops ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? ) | drops_lstar drops_weight drops_length drops_ext2 drops_lexs drops_lreq drops_drops |
|
generic relocation | lifts_bind ( ⬆*[?] ? ≡ ? ) | lifts_weight_bind lifts_lifts_bind |
|
|
lifts_vector ( ⬆*[?] ? ≡ ? ) | lifts_lifts_vector |
|
|
lifts ( ⬆*[?] ? ≡ ? ) | lifts_simple lifts_weight lifts_tdeq lifts_lifts |
|
ranged equivalence for local environments | lreq ( ? ≡[?] ? ) | lreq_length lreq_lreq |
|
generic entrywise extension | lexs ( ? ⦻*[?,?,?] ? ) | lexs_length lexs_lexs |
syntax | append for local environments | append ( ? @@ ? ) | append_length |
|
head equivalence for terms | theq ( ? ⩳[?,?] ? ) | theq_simple theq_tdeq theq_theq theq_simple_vector |
|
degree-based equivalence | tdeq_ext ( ? ≡[?,?] ? ) |
|
|
|
tdeq ( ? ≡[?,?] ? ) | tdeq_tdeq |
|
closures | cl_weight ( ♯{?,?,?} ) |
|
|
|
cl_restricted_weight ( ♯{?,?} ) |
|
|
global environments | genv |
|
|
local environments | lenv_ext2 |
|
|
|
lenv_length ( |?| ) |
|
|
|
lenv_weight ( ♯{?} ) |
|
|
|
lenv |
|
|
binders for local environments | ext2 | ext2_ext2 |
|
|
bind | bind_weight |
|
terms | term_vector ( Ⓐ?.? ) |
|
|
|
term_simple ( 𝐒⦃?⦄ ) |
|
|
|
term_weight ( ♯{?} ) |
|
|
|
term |
|
|
items | item_sd |
|
|
|
item_sh |
|
|
|
item |
|
|
atomic arities | aarity |
|