- additions in basic_2

[helm.git] / helm / www / lambda_delta / web / home / basic_2_blk.tbl

diff --git a/helm/www/lambda_delta/web/home/basic_2_blk.tbl b/helm/www/lambda_delta/web/home/basic_2_blk.tbl
index 8c4ee482733d1d38ac99250a069898dde70cf848..ed50adf79e14310e06514b8bfa869f724d4bb13d 100644 (file)
--- a/helm/www/lambda_delta/web/home/basic_2_blk.tbl
+++ b/helm/www/lambda_delta/web/home/basic_2_blk.tbl
@@ -9,30 +9,38 @@ table {
    } ]
    [ { "{X | Γ ⊢ X : W}" * } {
       class "wine" [
-         [ "typed abstraction **" ] [ "Γ ⊢ λW" ]
+         [ "local typed abstraction *" ] [ "Γ ⊢ +λW" ]
          [ "ⓐV" ] [ "→β" ] [ "no" ] [ "#i" ]
       ]
       class "magenta" [
-         [ "typed declaration ***" ] [ "Γ ⊢ pλW" ] 
-        [ "no" ] [ "no" ] [ "no" ] [ "$p" ]
+         [ "local typed declaration **" ] [ "Γ ⊢ -λW" ]
+         [ "ⓐV" ] [ "→β" ] [ "no" ] [ "#i" ]
       ]
       class "prune" [
+         [ "global typed declaration ***" ] [ "Γ ⊢ pλW" ] 
+        [ "no" ] [ "no" ] [ "no" ] [ "$p" ]
+      ]
+      class "blue" [
          [ "native type annotation *" ] [ "Γ ⊢ ⓝW" ]
         [ "no" ] [ "no" ] [ "yes" ] [ "no" ]
       ]
    } ]
    [ { "{X | Γ ⊢ X = V}" * } {
-      class "blue" [
-         [ "local abbreviation **" ] [ "Γ ⊢ δV" ] 
+      class "sky" [
+         [ "local abbreviation *" ] [ "Γ ⊢ +δV" ] 
          [ "no" ] [ "local →δ" ] [ "yes" ] [ "#i" ]
       ]
-      class "sky" [
-         [ "global abbreviation ***" ] [ "Γ ⊢ pδV" ]
+      class "cyan" [
+         [ "local definition **" ] [ "Γ ⊢ -δV" ] 
+         [ "no" ] [ "local →δ" ] [ "no" ] [ "#i" ]
+      ]      
+      class "water" [
+         [ "global definition ***" ] [ "Γ ⊢ pδV" ]
          [ "no" ] [ "global →δ" ] [ "no" ] [ "$p" ]
       ]
    } ]
    [ { "no" * } {
-      class "cyan" [
+      class "green" [
          [ "sort ****" ] [ "Γ ⊢ ⋆k" ]
         [ "no" ] [ "no" ] [ "no" ] [ "no" ]
       ]
@@ -42,4 +50,3 @@ table {
 class "text" { 0 } { 2 * }
 
 class "plane" { 1 }
-