]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/www/lambda_delta/web/home/ld_basic_2.tbl
Basic_2 update ...
[helm.git] / helm / www / lambda_delta / web / home / ld_basic_2.tbl
index bcbb90b8b0ba6393019f769e809b15ca2c206116..89cc5e535338783654c0dd1553b9bc046c1cfa6e 100644 (file)
@@ -9,82 +9,100 @@ table {
         ]
      }
    ]
+   class "prune"
+   [ { "functional" * } {
+        [ { "unfold" * } { 
+             [ "lift" "subst" * ]
+         }
+        ]
+     }
+   ]
    class "blue"
    [ { "examples" * } {
-         [ { "" * } {
-             [ "" * ]
-          }
-         ]
-      }
+        [ { "" * } {
+            [ "" * ]
+         }
+        ]
+     }
    ]
    class "sky"
    [ { "native typing" * } {
-         [ { "" * } {
-             [ "nty" * ]
-          }
-         ]
-      }
+        [ { "" * } {
+            [ "nty" * ]
+         }
+        ]
+     }
    ]
    class "cyan"
    [ { "conversion" * } {
-         [ { "context-sensitive conversion" * } {
-             [ "cpcs" * ]
-          }
-         ]
-      }
+        [ { "context-sensitive conversion" * } {
+            [ "cpcs" * ]
+         }
+        ]
+     }
    ]
    class "water"
    [ { "computation" * } {
-         [ { "strongly normalizing computation" * } {
-             [ "csn" * ]
-          }
-         ]
-         [ { "context-sensitive computation" * } {
-             [ "cprs" * ]
-          }
-         ]
-      }
+        [ { "strongly normalizing computation" * } {
+            [ "lsubcs" * ]
+            [ "csn" "csn_cr" "csn_aarity" * ]
+         }
+        ]
+        [ { "context-sensitive computation" * } {
+            [ "cprs" * ]
+         }
+        ]
+        [ { "support for abstract comptation properties" * } {
+            [ "lsubc" * ]
+            [ "acp" "acp_cr" * ]
+          }
+       ]
+     }
    ]
    class "green"
    [ { "reducibility" * } {
-         [ { "context-sensitive reduction" * } {
-             [ "lcpr" * ]
-             [ "cpr" "cpr_lift" "cpr_ltpr" "cpr_cpr" * ]
-          }
-         ]
-         [ { "context-free normal forms" * } {
-             [ "tnf" * ]
-           }
-        ]
-         [ { "context-free reduction" * } {
-             [ "ltpr" "ltpr_ldrop" * ]
-             [ "tpr"  "tpr_lift" "tpr_tpss" "tpr_tpr" * ]
-           }
-        ]
-         [ { "context-free reducible forms" * } {
-             [ "trf" * ]
-           }
-        ]
-      }
+        [ { "context-sensitive reduction" * } {
+            [ "lcpr" * ]
+            [ "cpr" "cpr_lift" "cpr_ltpr" "cpr_cpr" * ]
+         }
+        ]
+        [ { "context-free normal forms" * } {
+            [ "twhnf" "tnf" * ]
+          }
+       ]
+        [ { "context-free reduction" * } {
+            [ "ltpr" "ltpr_ldrop" * ]
+            [ "tpr"  "tpr_lift" "tpr_tpss" "tpr_tpr" * ]
+          }
+       ]
+        [ { "context-free reducible forms" * } {
+            [ "trf" * ]
+          }
+       ]
+     }
    ]
    class "grass"
    [ { "static typing" * } {
-         [ { "atomic arity ass." * } {
-             [ "aaa" "aaa_lift" "aaa_aaa" * ]
-          }
-         ]
-         [ { "static type ass." * } {
-             [ "sty" "sty_lift" "sty_sty" * ]
-           }
-        ]
-      }
-   ]   
+        [ { "static type ass." * } {
+            [ "sty" "sty_lift" "sty_sty" * ]
+          }
+       ]
+        [ { "atomic arity ass." * } {
+            [ "aaa" "aaa_lift" "aaa_aaa" * ]
+         }
+        ]
+        [ { "parameters" * } {
+             [ "sh" * ]
+          }
+        ]
+     }
+   ]
    class "yellow"
    [ { "unfold" * } {
-        [ { "telescopic substitution" * } {
-            [ "tsubst" * ]
+        [ { "term inverse relocation" * } {
+            [ "delift" "delift_lift" * ]
           }
-       ]       
+       ]
        [ { "partial unfold" * } {
              [ "ltpss" "ltpss_ldrop" "ltpss_tps" "ltpss_ltpss" * ] 
             [ "tpss" "tpss_lift" "tpss_tpss" "tpss_ltps" * ]
@@ -99,7 +117,11 @@ table {
             [ "tps" "tps_lift" "tps_tps" * ]
           }
        ]
-       [ { "local env. dropping" * } {
+       [ { "global env. slicing" * } {
+             [ "gdrop" * ]
+          }
+       ]
+       [ { "local env. slicing" * } {
              [ "ldrop" "ldrop_ldrop" * ]
           }
        ]
@@ -133,10 +155,6 @@ table {
              [ "aarity" * ]
          }
        ] 
-        [ { "parameters" * } {
-             [ "sh" * ]
-          }
-        ]
      }
    ]
 }