helm/www/lambda_delta/web/home/basic_2_blk.tbl

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