+++ /dev/null
-name "basic_1_src"
-
-table uri "static/coq/lambdadelta/basic_1/" ext ".txt" {
- class "gray"
- [ { "component" * } {
- [ { "plane" * } {
- [ "files" * ]
- }
- ]
- }
- ]
- class "wine"
- [ { "examples" * } {
- [ { "terms with special features" * } {
- [ @@"levels_ex0" + @@"ty3_ex1" + @@"nf2_ex2" * ]
- }
- ]
- }
- ]
- class "magenta"
- [ { "" * } {
- [ { "" * } {
- [ "" * ]
- }
- ]
- }
- ]
-(*
- [ { "higher order dynamic typing" * } {
- [ { "higher order native type assignment" * } {
- [ "ntas ( ⦃?,?⦄ ⊢ ? :* ? )" "nta_lift" * ]
- }
- ]
- }
- ]
-*)
- class "prune"
- [ { "dynamic typing" * } {
- [ { "well-formed contexts" * } {
- [ @@"wf3_defs" @@"wf3_props" * ]
- }
- ]
- [ { "context ref. for native type assignment" * } {
- [ @@"csubt_defs" @@"csubt_props" + @@"csubt_arity_props" * ]
- }
- ]
- [ { "native type assignment" * } {
- [ @@"ty3_defs" @@"ty3_props" + @@"ty3_gen" + @@"ty3_gen_context" + @@"ty3_gen_nf2" + @@"ty3_lift" + @@"ty3_subst0" + @@"ty3_arity_props" + @@"ty3_nf2_gen" + @@"ty3_sred" + @@"ty3_sred_props" + @@"ty3_dec" * ]
- }
- ]
- }
- ]
- class "blue"
- [ { "equivalence" * } {
- [ { "context-sensitive equivalence" * } {
- [ @@"pc3_defs" @@"pc3_props" + @@"pc3_gen" + @@"pc3_gen_context" + @@"pc3_subst0" * ]
- }
- ]
- [ { "context-free equivalence" * } {
- [ @@"pc1_defs" @@"pc1_props" * ]
- }
- ]
- }
- ]
- class "sky"
- [ { "" * } {
- [ { "" * } {
- [ "" * ]
- }
- ]
- }
- ]
- class "cyan"
- [ { "computation" * } {
- [ { "context ref. for reducibility" * } {
- [ @@"csubc_defs" @@"csubc_props" * ]
- }
- ]
- [ { "reducibility" * } {
- [ @@"sc3_defs" @@"sc3_props" + @@"sc3_arity" * ]
- }
- ]
- [ { "strongly normalizing computation" * } {
- [ @@"sn3_defs" @@"sn3_gen" + @@"sn3_props" * ]
- }
- ]
- [ { "context-sensitive computation" * } {
- [ @@"pr3_defs" @@"pr3_props" + @@"pr3_gen" + @@"pr3_gen_context" + @@"pr3_iso" + @@"pr3_subst1" + @@"pr3_confluence" * ]
- }
- ]
- [ { "context-free computation" * } {
- [ @@"pr1_defs" @@"pr1_props" + @@"pr1_confluence" * ]
- }
- ]
- }
- ]
- class "water"
- [ { "reduction" * } {
- [ { "normal forms for context-sensitive reduction" * } {
- [ @@"nf2_defs" @@"nf2_props" + @@"nf2_gen" + @@"nf2_dec" * ]
- }
- ]
- [ { "context-sensitive reduction" * } {
- [ @@"pr2_defs" @@"pr2_gen" + @@"pr2_gen_context" + @@"pr2_lift" + @@"pr2_subst1" + @@"pr2_confluence" * ]
- }
- ]
- [ { "normal forms for context-free reduction" * } {
- [ "" @@"nf0_dec" * ]
- }
- ]
- [ { "context-free reduction" * } {
- [ @@"wcpr0_defs" * ]
- [ @@"pr0_defs" @@"pr0_gen" + @@"pr0_lift" + @@"pr0_subst0" + @@"pr0_subst1" + @@"pr0_confluence" * ]
- }
- ]
- }
- ]
- class "green"
- [ { "unfold" * } {
- [ { "iterated static type assignment" * } {
- [ @@"sty1_defs" @@"sty1_props" * ]
- }
- ]
- }
- ]
- class "grass"
- [ { "static typing" * } {
- [ { "static type assignment" * } {
- [ @@"sty0_defs" @@"sty0_props" * ]
- }
- ]
- [ { "context ref. for binary arity assignment" * } {
- [ @@"csuba_defs" @@"csuba_props" * ]
- }
- ]
- [ { "binary arity assignment" * } {
- [ @@"arity_defs" @@"arity_props" + @@"arity_gen" + @@"arity_subst0" + @@"arity_sred" * ]
- }
- ]
- [ { "binary arity" * } {
- [ @@"levels_defs" + @@"llt_defs" + @@"aprem_defs" * ]
- }
- ]
- [ { "parameters" * } {
- [ @@"parameter_defs" * ]
- }
- ]
- [ { "basic context ref." * } {
- [ @@"csubv_defs" * ]
- }
- ]
- }
- ]
- class "yellow"
- [ { "multiple substitution" * } {
- [ { "iterated context slicing" * } {
- [ @@"drop1_defs" @@"drop1_props" * ]
- }
- ]
- [ { "generic term relocation" * } {
- [ @@"lift1_defs" @@"lift1_props" * ]
- }
- ]
- }
- ]
- class "orange"
- [ { "substitution" * } {
- [ { "ordinary substitution" * } {
- [ @@"subst_defs" @@"subst_props" * ]
- [ @@"csubst1_defs" @@"csubst1_props" * ]
- [ @@"subst1_defs" @@"subst1_gen" + @@"subst1_lift" + @@"subst1_subst1" + @@"subst1_confluence" * ]
- }
- ]
- [ { "normal forms for ordinary strict substitution" * } {
- [ "" @@"dnf_dec" * ]
- }
- ]
- [ { "ordinary strict substitution" * } {
- [ @@"fsubst0_defs" * ]
- [ @@"csubst0_defs" * ]
- [ @@"subst0_defs" @@"subst0_gen" + @@"subst0_tlt" + @@"subst0_lift" + @@"subst0_subst0" + @@"subst0_confluence" * ]
- }
- ]
- [ { "basic local env. slicing" * } {
- [ @@"getl_defs" @@"getl_props" * ]
- [ @@"drop_defs" @@"drop_props" * ]
- }
- ]
- [ { "basic term relocation" * } {
- [ @@"lift_defs" @@"lift_props" + @@"lift_gen" + @@"lift_tlt" * ]
- }
- ]
- }
- ]
- class "red"
- [ { "grammar" * } {
- [ { "closures" * } {
- [ @@"flt_defs" * ]
- }
- ]
- [ { "contexts" * } {
- [ @@"contexts_defs" + @@"clt_defs" + @@"ctail_defs" + @@"app_defs" + @@"cnt_defs" * ]
- }
- ]
- [ { "terms" * } {
- [ @@"tlist_defs" * ]
- [ @@"terms_defs" + @@"tlt_defs" + @@"iso_defs" * ]
- }
- ]
- }
- ]
-}
-
-class "top" { * }
-
-class "capitalize italic" { 0 }
-
-class "italic" { 1 }