]> matita.cs.unibo.it Git - helm.git/blob - helm/coq-contribs/lambdadelta/web/basic_1_blk.tbl
milestone update in basic_2
[helm.git] / helm / coq-contribs / lambdadelta / web / basic_1_blk.tbl
1 name "basic_1_blk"
2
3 table {
4    class "gray" [ { "domain" * } {
5       [
6          [ "block" ] [ "leader" ]
7          [ "→ζ *" ] [ "annotator (with →ϵ *)" ]
8          [ "applicator (with →θ *)" ] [ "reference *" ] [ "reduction" ]
9       ]
10    } ]
11    [ { "{X | Γ ⊢ ⊤}" * } {
12       class "wine" [
13          [ "exclusion" ] [ "Γ ⊢ χ" ]
14          [ "yes" ] [ "no" ] [ "no" ] [ "no" ] [ "no" ]
15       ]
16    } ]
17    [ { "{X | Γ ⊢ X : W}" * } {
18       class "magenta" [
19          [ "typed abstraction" ] [ "Γ ⊢ λW" ]
20          [ "no" ] [ "<W>" ] [ "(V)" ] [ "#i" ] [ "→β *" ]
21       ]
22    } ]
23    [ { "{X | Γ ⊢ X = V}" * } {
24       class "prune" [
25          [ "abbreviation" ] [ "Γ ⊢ δV" ]
26          [ "yes" ] [ "no" ] [ "no" ] [ "#i" ] [ "→δ" ] 
27       ]
28    } ]
29    [ { "no" * } {
30       class "blue" [
31          [ "sort" ] [ "Γ ⊢ ⋆k" ]
32          [ "no" ] [ "no" ] [ "no" ] [ "no" ] [ "no" ]
33       ]
34    } ]
35 }
36
37 class "top"    { * }
38
39 class "italic" { 1 }