helm/coq-contribs/lambdadelta/web/basic_1_src.tbl

   1 name "basic_1_src"
   2
   3 table uri "static/coq/lambdadelta/basic_1/" ext ".txt" {
   4    class "gray"
   5    [ { "component" * } {
   6         [ { "plane" * } {
   7              [ "files" * ]
   8           }
   9         ]
  10      }
  11    ]
  12    class "wine"
  13    [ { "examples" * } {
  14         [ { "terms with special features" * } {
  15              [ @@"levels_ex0" + @@"ty3_ex1" + @@"nf2_ex2" * ]
  16           }
  17         ]
  18      }
  19    ]
  20    class "magenta"
  21    [ { "" * } {
  22         [ { "" * } {
  23              [ "" * ]
  24           }
  25         ]
  26      }
  27    ]
  28 (*
  29    [ { "higher order dynamic typing" * } {
  30         [ { "higher order native type assignment" * } {
  31              [ "ntas ( ⦃?,?⦄ ⊢ ? :* ? )" "nta_lift" * ]
  32           }
  33         ]
  34      }
  35    ]
  36 *)
  37    class "prune"
  38    [ { "dynamic typing" * } {
  39         [ { "well-formed contexts" * } {
  40              [ @@"wf3_defs" @@"wf3_props" * ]
  41           }
  42         ]
  43         [ { "context ref. for native type assignment" * } {
  44              [ @@"csubt_defs" @@"csubt_props" + @@"csubt_arity_props" * ]
  45           }
  46         ]
  47         [ { "native type assignment" * } {
  48              [ @@"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" * ]
  49           }
  50         ]
  51      }
  52    ]
  53    class "blue"
  54    [ { "equivalence" * } {
  55         [ { "context-sensitive equivalence" * } {
  56              [ @@"pc3_defs" @@"pc3_props" + @@"pc3_gen" + @@"pc3_gen_context" + @@"pc3_subst0" * ]
  57           }
  58         ]
  59         [ { "context-free equivalence" * } {
  60              [ @@"pc1_defs" @@"pc1_props" * ]
  61           }
  62         ]
  63      }
  64    ]
  65    class "sky"
  66    [ { "" * } {
  67         [ { "" * } {
  68              [ "" * ]
  69           }
  70         ]
  71      }
  72    ]
  73    class "cyan"
  74    [ { "computation" * } {
  75         [ { "context ref. for reducibility" * } {
  76              [ @@"csubc_defs" @@"csubc_props" * ]
  77           }
  78         ]
  79         [ { "reducibility" * } {
  80              [ @@"sc3_defs" @@"sc3_props" + @@"sc3_arity" * ]
  81           }
  82         ]
  83         [ { "strongly normalizing computation" * } {
  84              [ @@"sn3_defs" @@"sn3_gen" + @@"sn3_props" * ]
  85           }
  86         ]
  87         [ { "context-sensitive computation" * } {
  88              [ @@"pr3_defs" @@"pr3_props" + @@"pr3_gen" + @@"pr3_gen_context" + @@"pr3_iso" + @@"pr3_subst1" + @@"pr3_confluence" * ]
  89           }
  90         ]
  91         [ { "context-free computation" * } {
  92              [ @@"pr1_defs" @@"pr1_props" + @@"pr1_confluence" * ]
  93           }
  94         ]
  95      }
  96    ]
  97    class "water"
  98    [ { "reduction" * } {
  99         [ { "normal forms for context-sensitive reduction" * } {
 100              [ @@"nf2_defs" @@"nf2_props" + @@"nf2_gen" + @@"nf2_dec" * ]
 101           }
 102         ]
 103         [ { "context-sensitive reduction" * } {
 104              [ @@"pr2_defs" @@"pr2_gen" + @@"pr2_gen_context" + @@"pr2_lift" + @@"pr2_subst1" + @@"pr2_confluence" * ]
 105           }
 106         ]
 107         [ { "normal forms for context-free reduction" * } {
 108              [ "" @@"nf0_dec" * ]
 109           }
 110         ]
 111         [ { "context-free reduction" * } {
 112              [ @@"wcpr0_defs" * ]
 113              [ @@"pr0_defs" @@"pr0_gen" + @@"pr0_lift" + @@"pr0_subst0" + @@"pr0_subst1" + @@"pr0_confluence" * ]
 114           }
 115         ]
 116      }
 117    ]
 118    class "green"
 119    [ { "unfold" * } {
 120         [ { "iterated static type assignment" * } {
 121              [ @@"sty1_defs" @@"sty1_props" * ]
 122           }
 123         ]
 124      }
 125    ]
 126    class "grass"
 127    [ { "static typing" * } {
 128         [ { "static type assignment" * } {
 129              [ @@"sty0_defs" @@"sty0_props" * ]
 130           }
 131         ]
 132         [ { "context ref. for binary arity assignment" * } {
 133              [ @@"csuba_defs" @@"csuba_props" * ]
 134           }
 135         ]
 136         [ { "binary arity assignment" * } {
 137              [ @@"arity_defs" @@"arity_props" + @@"arity_gen" + @@"arity_subst0" + @@"arity_sred" * ]
 138           }
 139         ]
 140         [ { "binary arity" * } {
 141              [ @@"levels_defs" + @@"llt_defs" + @@"aprem_defs" * ]
 142           }
 143         ]
 144         [ { "parameters" * } {
 145              [ @@"parameter_defs" * ]
 146           }
 147         ]
 148         [ { "basic context ref." * } {
 149              [ @@"csubv_defs" * ]
 150           }
 151         ]
 152      }
 153    ]
 154    class "yellow"
 155    [ { "multiple substitution" * } {
 156         [ { "iterated context slicing" * } {
 157              [ @@"drop1_defs" @@"drop1_props" * ]
 158           }
 159         ]
 160         [ { "generic term relocation" * } {
 161              [ @@"lift1_defs" @@"lift1_props" * ]
 162           }
 163         ]
 164      }
 165    ]
 166    class "orange"
 167    [ { "substitution" * } {
 168         [ { "ordinary substitution" * } {
 169              [ @@"subst_defs" @@"subst_props" * ]
 170              [ @@"csubst1_defs" @@"csubst1_props" * ]
 171              [ @@"subst1_defs" @@"subst1_gen" + @@"subst1_lift" + @@"subst1_subst1" + @@"subst1_confluence" * ]
 172           }
 173         ]
 174         [ { "normal forms for ordinary strict substitution" * } {
 175              [ "" @@"dnf_dec" * ]
 176           }
 177         ]
 178         [ { "ordinary strict substitution" * } {
 179              [ @@"fsubst0_defs" * ]
 180              [ @@"csubst0_defs" * ]
 181              [ @@"subst0_defs" @@"subst0_gen" + @@"subst0_tlt" + @@"subst0_lift" + @@"subst0_subst0" + @@"subst0_confluence" * ]
 182           }
 183         ]
 184         [ { "basic local env. slicing" * } {
 185              [ @@"getl_defs" @@"getl_props" * ]
 186              [ @@"drop_defs" @@"drop_props" * ]
 187           }
 188         ]
 189         [ { "basic term relocation" * } {
 190              [ @@"lift_defs" @@"lift_props" + @@"lift_gen" + @@"lift_tlt" * ]
 191           }
 192         ]
 193      }
 194    ]
 195    class "red"
 196    [ { "grammar" * } {
 197         [ { "closures" * } {
 198              [ @@"flt_defs" * ]
 199           }
 200         ]
 201         [ { "contexts" * } {
 202              [ @@"contexts_defs" + @@"clt_defs" + @@"ctail_defs" + @@"app_defs" + @@"cnt_defs" * ]
 203           }
 204         ]
 205         [ { "terms" * } {
 206              [ @@"tlist_defs" * ]
 207              [ @@"terms_defs" + @@"tlt_defs" + @@"iso_defs" * ]
 208           }
 209         ]
 210      }
 211    ]
 212 }
 213
 214 class "top"               { * }
 215
 216 class "capitalize italic" { 0 }
 217
 218 class "italic"            { 1 }