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           }
  17         ]
  18         [ { "denotational equivalence" * } {
  19              [ "deq" + "( ? ⊢ ? ≗{?} ? )" "deq_cpr" * ]
  20           }
  21         ]
  22         [ { "local environment interpretation" * } {
  23              [ "li" + "( ? ϵ ⟦?⟧{?}[?] )" "li_vpushs" * ]
  24           }
  25         ]
  26         [ { "multiple evaluation push" * } {
  27              [ "vpushs" + "( ?⨁{?}[?]? ≘ ? )" "vpush_fold" * ]
  28           }
  29         ]
  30         [ { "evaluation equivalence" * } {
  31              [ "veq" + "( ? ≗{?} ? )" "veq_lifts" * ]
  32           }
  33         ]
  34         [ { "model declaration" * } {
  35              [ "model" + "( ? ≗{?} ? )" + "( ? @{?} ? )" + "( ⟦?⟧{?}[?,?] )"
  36                "model_vpush" + "( ⫯{?}[?←?]? )"
  37                "model_props"
  38                * ]
  39           }
  40         ]
  41      }
  42    ]
  43 (*
  44    class "yellow"
  45    [ { "MLTT1" * } {
  46         [ { "" * } {
  47              [ "genv_primitive" "judgment" * ]
  48           }
  49         ]
  50      }
  51    ]
  52 *)
  53    class "orange"
  54    [ { "functional" * } {
  55         [ { "multiple filling" * } {
  56              [ "mf" + "( ●[?,?]? )" "mf_exeq" "mf_lifts" "mf_cpr" *]
  57              [ "mf_vpush" + "( ⇡[?←?]? )" "mf_vpush_exteq" "mf_vpush_vlift" * ]
  58              [ "mf_vlift" + "( ⇡[?]? )" "mf_vlift_exteq" * ]
  59              [ "mf_v" * ]
  60           }
  61         ]
  62         [ { "relocation" * } {
  63              [ "flifts_basic" + "( ↑[?,?]? )" "flifts_flifts_basic" * ]
  64              [ "flifts" + "( ↑*[?]? )" + "( ↑[?]? )" "flifts_flifts" * ]
  65           }
  66         ]
  67      }
  68    ]
  69    class "red"
  70    [ { "examples" * } {
  71         [ { "terms with special features" * } {
  72              [ (* "ex_sta_ldec" + *) "ex_cpr_omega" (* + "ex_fpbg_refl" + "ex_snv_eta" *) * ]
  73           }
  74         ]
  75      }
  76    ]
  77 }
  78
  79 class "top"               { * }
  80
  81 class "capitalize italic" { 0 }
  82
  83 class "italic"            { 1 }
  84 (*
  85         [ { "evaluation drop" * } {
  86              [ "vdrop" + "( ⫰{?}? )" + "( ⫰{?}[?]? )" "vdrop_vlift" * ]
  87           }
  88         ]
  89         [ { "reduction and type machine" * } {
  90              [ "rtm" "rtm_step ( ? ⇨ ? )" * ]
  91           }
  92         ]
  93 *)