]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/www/lambda_delta/web/home/basic_2_src.tbl
additions to basic_2
[helm.git] / helm / www / lambda_delta / web / home / basic_2_src.tbl
index be86628b0cbc9e19e5082b2ab51155173b42c267..d827e6f9a7f6cc1284d5e5c49eae169d4f03ae01 100644 (file)
@@ -9,7 +9,7 @@ table {
         ]
      }
    ]
-   class "prune"
+   class "wine"
    [ { "examples" * } {
         [ { "" * } {
             [ "" * ]
@@ -17,19 +17,27 @@ table {
         ]
      }
    ]
-   class "blue"
+   class "magenta"
+   [ { "higher order dynamic typing" * } {
+        [ { "higher order native type assignment" * } {
+            [ "ntas ( ⦃?,?⦄ ⊢ ? :* ? )" "nta_lift" * ]
+         }
+        ]
+     }
+   ]   
+   class "prune"
    [ { "dynamic typing" * } {
         [ { "local env. ref. for native type assignment" * } {
             [ "lsubn ( ? ⊢ ? :⊑ ? )" "lsubn_ldrop" "lsubn_cpcs" "lsubn_nta" * ]
          }
         ]
         [ { "native type assignment" * } {
-            [ "nta ( ⦃?,?⦄ ⊢ ? : ? )" "nta_alt ( ⦃?,?⦄ ⊢ ? :: ? )" "nta_lift" "nta_ltpss" "nta_thin" "nta_sta" "nta_ltpr" "nta_nta" * ]
+            [ "nta ( ⦃?,?⦄ ⊢ ? : ? )" "nta_alt ( ⦃?,?⦄ ⊢ ? :: ? )" "nta_lift" "nta_ltpss" "nta_thin" "nta_aaa" "nta_sta" "nta_ltpr" "nta_nta" * ]
          }
         ]
      }
    ]
-   class "sky"
+   class "blue"
    [ { "equivalence" * } {
         [ { "context-sensitive equivalence" * } {
             [ "lcpcs ( ? ⊢ ⬌* ? )" "lcpcs_aaa" "lcpcs_lcprs" "lcpcs_lcpcs" * ]
@@ -38,7 +46,7 @@ table {
         ]
      }
    ]
-   class "cyan"
+   class "sky"
    [ { "conversion" * } {
         [ { "context-sensitive conversion" * } {
             [ "lcpc ( ? ⊢ ⬌ ? )" "lcpc_lcpc" * ]        
@@ -47,7 +55,7 @@ table {
         ]
      }
    ]
-   class "water"
+   class "cyan"
    [ { "computation" * } {
         [ { "weakly normalizing computation" * } {
             [ "cpe ( ? ⊢ ➡* 𝐍⦃?⦄ )" "cpe_cpe" * ]
@@ -73,7 +81,7 @@ table {
        ]
      }
    ]
-   class "green"
+   class "water"
    [ { "reducibility" * } {
         [ { "context-sensitive normal forms" * } {
             [ "cnf ( ? ⊢ 𝐍⦃?⦄ )" "cnf_lift" * ]
@@ -99,6 +107,14 @@ table {
        ]
      }
    ]
+   class "green"
+   [ { "unwind" * } {
+        [ { "" * } {
+            [ "" * ]
+         }
+        ]
+     }
+   ]
    class "grass"
    [ { "static typing" * } {
         [ { "static type assignment" * } {