category | objects |
|
|
|
|
|
sizes | files | 83 | characters | 55955 | nodes | 191279 |
propositions | theorems | 33 | lemmas | 211 | total | 244 |
concepts | declared | 15 | defined | 23 | total | 38 |
component | plane | files |
|
|
|
relocation | ranged equivalence for closures | freq ( ⦃?,?,?⦄ ≡ ⦃?,?,?⦄ ) | freq_freq |
|
|
|
context-sensitive free variables | frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? ) | frees_weight frees_lreq frees_frees |
|
|
|
generic slicing for local environments | drops_vector ( ⬇*[?,?] ? ≡ ? ) |
|
|
|
|
|
drops ( ⬇*[?,?] ? ≡ ? ) | drops_lstar drops_weight drops_length drops_ceq drops_lexs drops_lreq drops_drops |
|
|
|
generic relocation for terms | lifts_vector ( ⬆*[?] ? ≡ ? ) | lifts_lift_vector |
|
|
|
|
lifts ( ⬆*[?] ? ≡ ? ) | lifts_simple lifts_weight lifts_lifts |
|
|
|
ranged equivalence for local environments | lreq ( ? ≡[?] ? ) | lreq_length lreq_lreq |
|
|
|
generic entrywise extension of context-sensitive relations for terma | lexs ( ? ⦻*[?,?,?] ? ) | lexs_length lexs_lexs |
|
|
|
|
|
|
||
grammar | context-sensitive equivalences for terms | ceq | ceq_ceq |
|
|
|
same top term structure | tsts ( ? ≂ ? ) | tsts_tsts tsts_vector |
|
|
|
closures | cl_weight ( ♯{?,?,?} ) | cl_restricted_weight ( ♯{?,?} ) |
|
|
|
internal syntax | genv |
|
|
|
|
|
lenv | lenv_weight ( ♯{?} ) | lenv_length ( |?| ) | lenv_append ( ? @@ ? ) |
|
|
term | term_weight ( ♯{?} ) | term_simple ( 𝐒⦃?⦄ ) | term_vector ( Ⓐ?.? ) |
|
|
item |
|
|
|
|
external syntax | aarity |
|
|
|