]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/www/lambda_delta/web/home/ld_basic_2.tbl
new files started ...
[helm.git] / helm / www / lambda_delta / web / home / ld_basic_2.tbl
index 8480c70de4796ca4afb625f29958e3992d72f888..503c11d45c1ba4f9ed7329668b1471c6f88f7786 100644 (file)
@@ -9,64 +9,94 @@ table {
         ]
      }
    ]
+   class "blue"
+   [ { "examples" * } {
+        [ { "" * } {
+            [ "" * ]
+         }
+        ]
+     }
+   ]
    class "sky"
    [ { "native typing" * } {
-         [ { "" * } {
-             [ "nty" * ]
-          }
-         ]
-      }
+        [ { "" * } {
+            [ "nty" * ]
+         }
+        ]
+     }
    ]
    class "cyan"
    [ { "conversion" * } {
-         [ { "context-sensitive" * } {
-             [ "cpcs" * ]
-          }
-         ]
-      }
+        [ { "context-sensitive conversion" * } {
+            [ "cpcs" * ]
+         }
+        ]
+     }
    ]
    class "water"
    [ { "computation" * } {
-         [ { "strongly normalizing" * } {
-             [ "csn" * ]
-          }
-         ]
-         [ { "context-sensitive" * } {
-             [ "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"
-   [ { "reduction" * } {
-         [ { "context-sensitive" * } {
-             [ "lcpr" * ]
-             [ "cpr" "cpr_lift" "cpr_tpss" "cpr_cpr" * ]
-          }
-         ]
-         [ { "context-free" * } {
-             [ "ltpr" "ltpr_drop" * ]
-             [ "tpr"  "tpr_lift" "tpr_tpss" "tpr_tpr" * ]
-           }
-        ]
-      }
+   [ { "reducibility" * } {
+        [ { "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" * } {
-        [ { "partial" * } {
-             [ "ltpss" "ltpss_drop" "ltpss_tps" "ltpss_ltpss" * ] 
+        [ { "term inverse relocation" * } {
+            [ "delift" * ]
+          }
+       ]
+       [ { "partial unfold" * } {
+             [ "ltpss" "ltpss_ldrop" "ltpss_tps" "ltpss_ltpss" * ] 
             [ "tpss" "tpss_lift" "tpss_tpss" "tpss_ltps" * ]
           }
        ]
@@ -74,13 +104,13 @@ table {
    ]
    class "orange"   
    [ { "substitution" * } { 
-        [ { "parallel" * } {
-             [ "ltps" "ltps_drop" "ltps_tps" "ltps_ltps" * ]
+        [ { "parallel substitution" * } {
+             [ "ltps" "ltps_ldrop" "ltps_tps" "ltps_ltps" * ]
             [ "tps" "tps_lift" "tps_tps" * ]
           }
        ]
        [ { "local env. dropping" * } {
-             [ "drop" "drop_drop" * ]
+             [ "ldrop" "ldrop_ldrop" * ]
           }
        ]
         [ { "term relocation" * } {
@@ -113,10 +143,6 @@ table {
              [ "aarity" * ]
          }
        ] 
-        [ { "parameters" * } {
-             [ "sh" * ]
-          }
-        ]
      }
    ]
 }