- [ { "basic term relocation" * } {
- [ "lift_vector ( ⇧[?,?] ? ≡ ? )" "lift_lift_vector" * ]
- [ "lift ( ⇧[?,?] ? ≡ ? )" "lift_lift" * ]
- }
- ]
- }
- ]
- class "red"
- [ { "grammar" * } {
- [ { "equivalence for local environments" * } {
- [ "leq ( ? ≃[?,?] ? )" "leq_leq" * ]
- }
- ]
- [ { "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_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" * ]
- }
- ]
- }
- ]
-}
-
-class "component" { 0 }
-
-class "plane" { 1 }
-
-class "file" { 2 * }