matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl

   1 name "apps_2_src"
   2
   3 table {
   4    class "gray"
   5    [ { "component" * } {
   6         [ { "plane" * } {
   7              [ "files" * ]
   8           }
   9         ]
  10      }
  11    ]
  12    class "yellow"
  13    [ { "models" * } {
  14         [ { "term model" * } {
  15              [ "tm" + "( ⇡[?]? )" + "( ⇡[?←?]? )"
  16                "tm_exteq"
  17              * ]
  18           }
  19         ]
  20         [ { "denotational equivalence" * } {
  21              [ "deq" + "( ? ⊢ ? ≗{?} ? )" "deq_cpr" * ]
  22           }
  23         ]
  24         [ { "local environment interpretation" * } {
  25              [ "li" + "( ? ϵ ⟦?⟧{?}[?] )" "li_vpushs" * ]
  26           }
  27         ]
  28         [ { "multiple evaluation push" * } {
  29              [ "vpushs" + "( ?⨁{?}[?]? ≘ ? )" "vpush_fold" * ]
  30           }
  31         ]
  32         [ { "evaluation equivalence" * } {
  33              [ "veq" + "( ? ≗{?} ? )" "veq_lifts" * ]
  34           }
  35         ]
  36         [ { "model declaration" * } {
  37              [ "model" + "( ? ≗{?} ? )" + "( ? @{?} ? )" + "( ⟦?⟧{?}[?,?] )"
  38                "model_vpush" + "( ⫯{?}[?←?]? )"
  39                "model_props"
  40                * ]
  41           }
  42         ]
  43      }
  44    ]
  45 (*
  46    class "yellow"
  47    [ { "MLTT1" * } {
  48         [ { "" * } {
  49              [ "genv_primitive" "judgment" * ]
  50           }
  51         ]
  52      }
  53    ]
  54 *)
  55    class "orange"
  56    [ { "functional" * } {
  57 (*
  58         [ { "reduction and type machine" * } {
  59              [ "rtm" "rtm_step ( ? ⇨ ? )" * ]
  60           }
  61         ]
  62 *)
  63         [ { "relocation" * } {
  64              [ "flifts" + "( ↑*[?]? )" + "( ↑[?]? )"
  65                "flifts_basic" + "( ↑[?,?]? )"
  66              * ]
  67           }
  68         ]
  69      }
  70    ]
  71    class "red"
  72    [ { "examples" * } {
  73         [ { "terms with special features" * } {
  74              [ (* "ex_sta_ldec" + *) "ex_cpr_omega" (* + "ex_fpbg_refl" + "ex_snv_eta" *) * ]
  75           }
  76         ]
  77      }
  78    ]
  79 }
  80
  81 class "top"               { * }
  82
  83 class "capitalize italic" { 0 }
  84
  85 class "italic"            { 1 }
  86 (*
  87         [ { "evaluation drop" * } {
  88              [ "vdrop" + "( ⫰{?}? )" + "( ⫰{?}[?]? )" "vdrop_vlift" * ]
  89           }
  90         ]
  91 *)