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" ] [ "&lt;W&gt;" ] [ "(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 }