]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl
6f9d8a2e7860a03e7610bfed3385274f953cdbd4
[helm.git] / 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" + "( ? ⊢ ? ≗{?} ? )" "deq_cpr" * ]
16           }
17         ]
18         [ { "evaluation equivalence" * } {
19              [ "veq" + "( ? ≗{?} ? )" "veq_vdrop" "veq_li" "veq_lifts" * ]
20           }
21         ]
22         [ { "evaluation drop" * } {        
23              [ "vdrop" + "( ⫰{?}? )" + "( ⫰{?}[?]? )" "vdrop_vlift" * ]
24           }
25         ]
26         [ { "model declaration" * } {
27              [ "model" + "( ? ≗{?} ? )" + "( ? @{?} ? )" + "( ⟦?⟧{?}[?,?] )"
28                "model_vlift" + "( ⫯{?}[?]? )" + "( ⫯{?}[?←?]? )"
29                "model_props"
30                "model_li" + "( ? ϵ ⟦?⟧{?}[?] )"
31                "model_gi"
32                * ]
33           }
34         ]
35      }
36    ]
37 (*
38    class "yellow"
39    [ { "MLTT1" * } {
40         [ { "" * } {
41              [ "genv_primitive" "judgment" * ]
42           }
43         ]
44      }
45    ]
46    class "orange"
47    [ { "functional" * } {
48         [ { "reduction and type machine" * } {
49              [ "rtm" "rtm_step ( ? ⇨ ? )" * ]
50           }
51         ]
52         [ { "relocation" * } {
53              [ "lift ( ↑[?,?] ? )" * ]
54           }
55         ]
56      }
57    ]
58 *)
59    class "red"
60    [ { "examples" * } {
61         [ { "terms with special features" * } {
62              [ (* "ex_sta_ldec" + *) "ex_cpr_omega" (* + "ex_fpbg_refl" + "ex_snv_eta" *) * ]
63           }
64         ]
65      }
66    ]
67 }
68
69 class "top"               { * }
70
71 class "capitalize italic" { 0 }
72
73 class "italic"            { 1 }