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 "orange"
  13    [ { "models" * } {
  14         [ { "denotational equivalence" * } {
  15              [ "deq" + "( ? ⊢ ? ≗{?} ? )" * ]
  16           }
  17         ]
  18         [ { "evaluation equivalence" * } {
  19              [ "veq" + "( ? ≗{?} ? )" "veq_li" * ]
  20           }
  21         ]
  22         [ { "model declaration" * } {
  23              [ "model" + "( ? ≗{?} ? )" + "( ? @{?} ? )" + "( ⟦?⟧{?}[?,?] )"
  24                "model_push" + "( ⫯{?}[?] )" + "( ⫯{?}[?←?] )"
  25                "model_props"
  26                "model_li" + "( ? ϵ ⟦?⟧{?}[?] )"
  27                * ]
  28           }
  29         ]
  30      }
  31    ]
  32 (*
  33    class "yellow"
  34    [ { "MLTT1" * } {
  35         [ { "" * } {
  36              [ "genv_primitive" "judgment" * ]
  37           }
  38         ]
  39      }
  40    ]
  41    class "orange"
  42    [ { "functional" * } {
  43         [ { "reduction and type machine" * } {
  44              [ "rtm" "rtm_step ( ? ⇨ ? )" * ]
  45           }
  46         ]
  47         [ { "relocation" * } {
  48              [ "lift ( ↑[?,?] ? )" * ]
  49           }
  50         ]
  51      }
  52    ]
  53 *)
  54    class "red"
  55    [ { "examples" * } {
  56         [ { "terms with special features" * } {
  57              [ (* "ex_sta_ldec" + *) "ex_cpr_omega" (* + "ex_fpbg_refl" + "ex_snv_eta" *) * ]
  58           }
  59         ]
  60      }
  61    ]
  62 }
  63
  64 class "top"               { * }
  65
  66 class "capitalize italic" { 0 }
  67
  68 class "italic"            { 1 }