matita/matita/contribs/lambdadelta/basic_2/web/basic_2_blk.tbl

   1 name "basic_2_blk"
   2
   3 table {
   4    class "gray" [ { "domain" * } {
   5       [
   6          [ "block" ] [ "leader" ]
   7          [ "applicator (with →θ)*" ] [ "reduction" ] [ "→ζ *" ] [ "reference *" ]
   8       ]
   9    } ]
  10    [ { "{X | Γ ⊢ X : W}" * } {
  11       class "wine" [
  12          [ "local typed abstraction *" ] [ "Γ ⊢ +λW" ]
  13          [ "ⓐV" ] [ "→β" ] [ "no" ] [ "#i" ]
  14       ]
  15       class "magenta" [
  16          [ "local typed declaration **" ] [ "Γ ⊢ -λW" ]
  17          [ "ⓐV" ] [ "→β" ] [ "no" ] [ "#i" ]
  18       ]
  19       class "prune" [
  20          [ "global typed declaration ***" ] [ "Γ ⊢ pλW" ]
  21          [ "no" ] [ "no" ] [ "no" ] [ "$p" ]
  22       ]
  23       class "blue" [
  24          [ "native type annotation *" ] [ "Γ ⊢ ⓝW" ]
  25          [ "no" ] [ "no" ] [ "yes" ] [ "no" ]
  26       ]
  27    } ]
  28    [ { "{X | Γ ⊢ X = V}" * } {
  29       class "sky" [
  30          [ "local abbreviation *" ] [ "Γ ⊢ +δV" ]
  31          [ "no" ] [ "local →δ" ] [ "yes" ] [ "#i" ]
  32       ]
  33       class "cyan" [
  34          [ "local definition **" ] [ "Γ ⊢ -δV" ]
  35          [ "no" ] [ "local →δ" ] [ "no" ] [ "#i" ]
  36       ]
  37       class "water" [
  38          [ "global definition ***" ] [ "Γ ⊢ pδV" ]
  39          [ "no" ] [ "global →δ" ] [ "no" ] [ "$p" ]
  40       ]
  41    } ]
  42    [ { "no" * } {
  43       class "green" [
  44          [ "sort ****" ] [ "Γ ⊢ ⋆k" ]
  45          [ "no" ] [ "no" ] [ "no" ] [ "no" ]
  46       ]
  47    } ]
  48 }
  49
  50 class "top"    { * }
  51
  52 class "italic" { 1 }